File: interp/src/extract/JsInterpreter.ml (return to index)



Statistics:  
kind coverage
binding 180 / 236 (76%)
sequence 2 / 4 (50%)
for 0 / 0 (-%)
if/then 138 / 260 (53%)
try 0 / 0 (-%)
while 0 / 0 (-%)
match/function 563 / 780 (72%)
kind coverage
class expression 0 / 0 (-%)
class initializer 0 / 0 (-%)
class method 0 / 0 (-%)
class value 0 / 0 (-%)
toplevel expression 0 / 0 (-%)
lazy operator 0 / 0 (-%)



Source:

fold all unfold all
000001| open Datatypes
000002| open JsInit
000003| open JsNumber
000004| open JsPreliminary
000005| open JsPreliminaryAux
000006| open JsSyntax
000007| open JsSyntaxAux
000008| open JsSyntaxInfos
000009| open LibBool
000010| open LibInt
000011| open LibList
000012| open LibNat
000013| open LibOption
000014| open LibReflect
000015| open LibString
000016| open List0
000017| open Shared
000018| open String0
000019|  
000020| let __ = (*[11745]*)let rec f _ = (*[0]*)Obj.repr f in (*[11745]*)Obj.repr f
000021|  
000022| type result =
000023| | Coq_result_out of out
000024| | Coq_result_stuck
000025| | Coq_result_bottom
000026|  
000027| type result_void = result
000028|  
000029| (** val stuck_because : char list -> result **)
000030|  
000031| let stuck_because = (fun s ->
000032|   (*[0]*)print_endline ("Stuck because:\t" ^ Prheap.string_of_char_list s) ;
000033|   (*[0]*)Coq_result_stuck)
000034|  
000035| (** val stuck_heap : state -> char list -> result **)
000036|  
000037| let stuck_heap = (fun s message ->
000038|   (*[7]*)print_endline ("Stuck!\nState: " ^ Prheap.prstate true s
000039|     ^ "\nMessage:\t" ^ Prheap.string_of_char_list message) ;
000040|   (*[7]*)Coq_result_stuck)
000041|  
000042| (** val get_arg : int -> value list -> value **)
000043|  
000044| let get_arg =
000045|   (*[11745]*)get_nth (Coq_value_prim Coq_prim_undef)
000046|  
000047| (** val destr_list : 'a1 list -> 'a2 -> ('a1 -> 'a2) -> 'a2 **)
000048|  
000049| let destr_list l d f =
000050|   match l with
000051|   | [] -> (*[0]*)d
000052|   | a :: l0 -> (*[10494]*)f a
000053|  
000054| (** val if_bool_option :
000055|     'a1 -> bool option -> (unit -> 'a1) -> (unit -> 'a1) -> 'a1 **)
000056|  
000057| let if_bool_option d bo k1 k2 =
000058|   (*[95034]*)morph_option d (fun b -> (*[95034]*)if b then (*[42896]*)k1 () else (*[52138]*)k2 ()) bo
000059|  
000060| (** val if_bool_option_result :
000061|     bool option -> (unit -> result) -> (unit -> result) -> result **)
000062|  
000063| let if_bool_option_result bo k1 k2 =
000064|   (*[50146]*)if_bool_option (fun x ->
000065|     (*[0]*)stuck_because
000066|       ('['::('i'::('f'::('_'::('b'::('o'::('o'::('l'::('_'::('o'::('p'::('t'::('i'::('o'::('n'::('_'::('r'::('e'::('s'::('u'::('l'::('t'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('['::('N'::('o'::('n'::('e'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))
000067|     bo (fun x -> (*[18072]*)k1) (fun x -> (*[32074]*)k2) ()
000068|  
000069| (** val if_some : 'a1 option -> ('a1 -> result) -> result **)
000070|  
000071| let if_some op k =
000072|   match op with
000073|   | Some a -> (*[298579]*)k a
000074|   | None ->
000075|     (*[0]*)stuck_because
000076|       ('['::('i'::('f'::('_'::('s'::('o'::('m'::('e'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('['::('N'::('o'::('n'::('e'::(']'::('.'::[])))))))))))))))))))))))))))))
000077|  
000078| (** val if_ter : result -> (state -> res -> result) -> result **)
000079|  
000080| let if_ter o k =
000081|   match o with
000082|   | Coq_result_out o0 ->
000083|     (match o0 with
000084|      | Coq_out_div -> (*[0]*)o
000085|      | Coq_out_ter (s0, r) -> (*[686526]*)k s0 r)
000086|   | _ -> (*[21]*)o
000087|  
000088| (** val if_success_state :
000089|     resvalue -> result -> (state -> resvalue -> result) -> result **)
000090|  
000091| let if_success_state rv o k =
000092|   (*[649184]*)if_ter o (fun s0 r ->
000093|     match r.res_type with
000094|     | Coq_restype_normal ->
000095|       (*[628665]*)k s0 (res_overwrite_value_if_empty rv r).res_value
000096|     | Coq_restype_throw -> (*[19792]*)o
000097|     | _ ->
000098|       (*[713]*)Coq_result_out (Coq_out_ter (s0, (res_overwrite_value_if_empty rv r))))
000099|  
000100| (** val if_success : result -> (state -> resvalue -> result) -> result **)
000101|  
000102| let if_success =
000103|   (*[11745]*)if_success_state Coq_resvalue_empty
000104|  
000105| (** val if_void : result_void -> (state -> result) -> result **)
000106|  
000107| let if_void o k =
000108|   (*[81835]*)if_success o (fun s rv ->
000109|     match rv with
000110|     | Coq_resvalue_empty -> (*[81727]*)k s
000111|     | _ ->
000112|       (*[0]*)stuck_heap s
000113|         ('['::('i'::('f'::('_'::('v'::('o'::('i'::('d'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(']'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('v'::('o'::('i'::('d'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))
000114|  
000115| (** val if_not_throw : result -> (state -> res -> result) -> result **)
000116|  
000117| let if_not_throw o k =
000118|   (*[32040]*)if_ter o (fun s0 r ->
000119|     match r.res_type with
000120|     | Coq_restype_throw -> (*[6460]*)o
000121|     | _ -> (*[25573]*)k s0 r)
000122|  
000123| (** val if_any_or_throw :
000124|     result -> (result -> result) -> (state -> value -> result) -> result **)
000125|  
000126| let if_any_or_throw o k1 k2 =
000127|   (*[2457]*)if_ter o (fun s r ->
000128|     match r.res_type with
000129|     | Coq_restype_throw ->
000130|       (match r.res_value with
000131|        | Coq_resvalue_value v -> (*[911]*)k2 s v
000132|        | _ ->
000133|          (*[0]*)stuck_heap s
000134|            ('['::('i'::('f'::('_'::('a'::('n'::('y'::('_'::('o'::('r'::('_'::('t'::('h'::('r'::('o'::('w'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('a'::(' '::('n'::('o'::('n'::('-'::('v'::('a'::('l'::('u'::('e'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))
000135|     | _ -> (*[1546]*)k1 o)
000136|  
000137| (** val if_success_or_return :
000138|     result -> (state -> result) -> (state -> resvalue -> result) -> result **)
000139|  
000140| let if_success_or_return o k1 k2 =
000141|   (*[2517]*)if_ter o (fun s r ->
000142|     match r.res_type with
000143|     | Coq_restype_normal -> (*[1701]*)k1 s
000144|     | Coq_restype_return -> (*[581]*)k2 s r.res_value
000145|     | _ -> (*[235]*)o)
000146|  
000147| (** val if_normal_continue_or_break :
000148|     result -> (res -> bool) -> (state -> res -> result) -> (state -> res ->
000149|     result) -> result **)
000150|  
000151| let if_normal_continue_or_break o search_label k1 k2 =
000152|   (*[59]*)if_ter o (fun s r ->
000153|     match r.res_type with
000154|     | Coq_restype_normal -> (*[14]*)k1 s r
000155|     | Coq_restype_break ->
000156|       (*[15]*)if search_label r then (*[14]*)k2 s r else (*[1]*)Coq_result_out (Coq_out_ter (s, r))
000157|     | Coq_restype_continue ->
000158|       (*[26]*)if search_label r then (*[26]*)k1 s r else (*[0]*)Coq_result_out (Coq_out_ter (s, r))
000159|     | _ -> (*[4]*)Coq_result_out (Coq_out_ter (s, r)))
000160|  
000161| (** val if_break : result -> (state -> res -> result) -> result **)
000162|  
000163| let if_break o k =
000164|   (*[7]*)if_ter o (fun s r ->
000165|     (*[7]*)let default = Coq_out_ter (s, r) in
000166|     (match r.res_type with
000167|      | Coq_restype_break -> (*[1]*)k s r
000168|      | _ -> (*[6]*)Coq_result_out default))
000169|  
000170| (** val if_value : result -> (state -> value -> result) -> result **)
000171|  
000172| let if_value o k =
000173|   (*[157449]*)if_success o (fun s rv ->
000174|     match rv with
000175|     | Coq_resvalue_value v -> (*[157308]*)k s v
000176|     | _ ->
000177|       (*[0]*)stuck_heap s
000178|         ('['::('i'::('f'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))
000179|  
000180| (** val if_bool : result -> (state -> bool -> result) -> result **)
000181|  
000182| let if_bool o k =
000183|   (*[53667]*)if_value o (fun s v ->
000184|     match v with
000185|     | Coq_value_prim p ->
000186|       (match p with
000187|        | Coq_prim_bool b -> (*[53659]*)k s b
000188|        | _ ->
000189|          (*[0]*)stuck_heap s
000190|            ('['::('i'::('f'::('_'::('b'::('o'::('o'::('l'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('b'::('o'::('o'::('l'::('e'::('a'::('n'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[])))))))))))))))))))))))))))))))))))))))))
000191|     | Coq_value_object o0 ->
000192|       (*[0]*)stuck_heap s
000193|         ('['::('i'::('f'::('_'::('b'::('o'::('o'::('l'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('b'::('o'::('o'::('l'::('e'::('a'::('n'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[])))))))))))))))))))))))))))))))))))))))))
000194|  
000195| (** val if_success_primitive :
000196|     result -> (state -> prim -> result) -> result **)
000197|  
000198| let if_success_primitive o k =
000199|   (*[275]*)if_value o (fun s v ->
000200|     match v with
000201|     | Coq_value_prim w -> (*[227]*)k s w
000202|     | Coq_value_object o0 ->
000203|       (*[0]*)stuck_heap s
000204|         ('['::('i'::('f'::('_'::('s'::('u'::('c'::('c'::('e'::('s'::('s'::('_'::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(']'::(' '::('d'::('i'::('d'::('n'::('\''::('t'::(' '::('g'::('e'::('t'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))
000205|  
000206| (** val if_object : result -> (state -> object_loc -> result) -> result **)
000207|  
000208| let if_object o k =
000209|   (*[58274]*)if_value o (fun s v ->
000210|     match v with
000211|     | Coq_value_prim p ->
000212|       (*[0]*)stuck_heap s
000213|         ('['::('i'::('f'::('_'::('o'::('b'::('j'::('e'::('c'::('t'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('o'::('n'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::('.'::[]))))))))))))))))))))))))))))))))))
000214|     | Coq_value_object l -> (*[58274]*)k s l)
000215|  
000216| (** val if_string : result -> (state -> char list -> result) -> result **)
000217|  
000218| let if_string o k =
000219|   (*[11176]*)if_value o (fun s v ->
000220|     match v with
000221|     | Coq_value_prim p ->
000222|       (match p with
000223|        | Coq_prim_string s0 -> (*[11176]*)k s s0
000224|        | _ ->
000225|          (*[0]*)stuck_heap s
000226|            ('['::('i'::('f'::('_'::('s'::('t'::('r'::('i'::('n'::('g'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('o'::('n'::(' '::('a'::(' '::('n'::('o'::('n'::('-'::('s'::('t'::('r'::('i'::('n'::('g'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))
000227|     | Coq_value_object o0 ->
000228|       (*[0]*)stuck_heap s
000229|         ('['::('i'::('f'::('_'::('s'::('t'::('r'::('i'::('n'::('g'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('o'::('n'::(' '::('a'::(' '::('n'::('o'::('n'::('-'::('s'::('t'::('r'::('i'::('n'::('g'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))
000230|  
000231| (** val if_number : result -> (state -> number -> result) -> result **)
000232|  
000233| let if_number o k =
000234|   (*[23374]*)if_value o (fun s v ->
000235|     match v with
000236|     | Coq_value_prim p ->
000237|       (match p with
000238|        | Coq_prim_number n -> (*[23328]*)k s n
000239|        | _ ->
000240|          (*[0]*)stuck_heap s
000241|            ('['::('i'::('f'::('_'::('n'::('u'::('m'::('b'::('e'::('r'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('n'::('u'::('m'::('b'::('e'::('r'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))
000242|     | Coq_value_object o0 ->
000243|       (*[0]*)stuck_heap s
000244|         ('['::('i'::('f'::('_'::('n'::('u'::('m'::('b'::('e'::('r'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('w'::('i'::('t'::('h'::(' '::('n'::('o'::('n'::('-'::('n'::('u'::('m'::('b'::('e'::('r'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))
000245|  
000246| (** val if_primitive : result -> (state -> prim -> result) -> result **)
000247|  
000248| let if_primitive o k =
000249|   (*[10430]*)if_value o (fun s v ->
000250|     match v with
000251|     | Coq_value_prim w -> (*[10415]*)k s w
000252|     | Coq_value_object o0 ->
000253|       (*[0]*)stuck_heap s
000254|         ('['::('i'::('f'::('_'::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(']'::(' '::('c'::('a'::('l'::('l'::('e'::('d'::(' '::('o'::('n'::(' '::('a'::('n'::(' '::('o'::('b'::('j'::('e'::('c'::('t'::('.'::[]))))))))))))))))))))))))))))))))))))
000255|  
000256| (** val if_def_full_descriptor :
000257|     full_descriptor option -> 'a1 -> (full_descriptor -> 'a1) -> 'a1 **)
000258|  
000259| let if_def_full_descriptor o d k =
000260|   (*[523753]*)morph_option d k o
000261|  
000262| (** val convert_option_attributes :
000263|     attributes option -> full_descriptor option **)
000264|  
000265| let convert_option_attributes =
000266|   (*[11745]*)option_map (fun a -> (*[121922]*)Coq_full_descriptor_some a)
000267|  
000268| (** val out_error_or_cst :
000269|     state -> strictness_flag -> resvalue -> res -> out **)
000270|  
000271| let out_error_or_cst s str b r =
000272|   (*[898]*)if str then (*[874]*)Coq_out_ter (s, (res_throw b)) else (*[24]*)Coq_out_ter (s, r)
000273|  
000274| (** val out_error_or_void : state -> strictness_flag -> resvalue -> out **)
000275|  
000276| let out_error_or_void s str b =
000277|   (*[12]*)if str then (*[0]*)Coq_out_ter (s, (res_throw b)) else (*[12]*)out_void s
000278|  
000279| (** val build_error : state -> value -> value -> result **)
000280|  
000281| let build_error s vproto vmsg =
000282|   (*[6828]*)let o = object_new vproto ('E'::('r'::('r'::('o'::('r'::[]))))) in
000283|   (*[6828]*)let (l, s') = object_alloc s o in
000284|   (*[6828]*)if value_comparable vmsg (Coq_value_prim Coq_prim_undef)
000285|   then (*[6828]*)Coq_result_out (Coq_out_ter (s',
000286|          (res_ref (Coq_resvalue_value (Coq_value_object l)))))
000287|   else (*[0]*)(assert false) __
000288|  
000289| (** val run_error : state -> native_error -> result **)
000290|  
000291| let run_error s ne =
000292|   (*[6828]*)if_object
000293|     (build_error s (Coq_value_object (Coq_object_loc_prealloc
000294|       (Coq_prealloc_native_error_proto ne))) (Coq_value_prim Coq_prim_undef))
000295|     (fun s' l -> (*[6828]*)Coq_result_out (Coq_out_ter (s',
000296|     (res_throw (Coq_resvalue_value (Coq_value_object l))))))
000297|  
000298| (** val run_object_method :
000299|     (coq_object -> 'a1) -> state -> object_loc -> 'a1 **)
000300|  
000301| let run_object_method proj s l =
000302|   (*[1087537]*)proj (object_binds_pickable s l)
000303|  
000304| (** val object_properties_keys_as_list_pickable :
000305|     state -> object_loc -> prop_name list coq_Pickable **)
000306|  
000307| let object_properties_keys_as_list_pickable s l =
000308|   (*[0]*)LibList.map fst (Heap.to_list (run_object_method object_properties_ s l))
000309|  
000310| (** val run_object_heap_set_extensible :
000311|     bool -> state -> object_loc -> state **)
000312|  
000313| let run_object_heap_set_extensible b s l =
000314|   (*[0]*)let o = object_binds_pickable s l in
000315|   (*[0]*)object_write s l (object_set_extensible o b)
000316|  
000317| type runs_type = { runs_type_expr : (state -> execution_ctx -> expr ->
000318|                                     result);
000319|                    runs_type_stat : (state -> execution_ctx -> stat ->
000320|                                     result);
000321|                    runs_type_prog : (state -> execution_ctx -> prog ->
000322|                                     result);
000323|                    runs_type_call : (state -> execution_ctx -> prealloc ->
000324|                                     value list -> result);
000325|                    runs_type_call_full : (state -> execution_ctx ->
000326|                                          object_loc -> value -> value list ->
000327|                                          result) }
000328|  
000329| (** val runs_type_expr :
000330|     runs_type -> state -> execution_ctx -> expr -> result **)
000331|  
000332| let runs_type_expr x = (*[0]*)x.runs_type_expr
000333|  
000334| (** val runs_type_stat :
000335|     runs_type -> state -> execution_ctx -> stat -> result **)
000336|  
000337| let runs_type_stat x = (*[0]*)x.runs_type_stat
000338|  
000339| (** val runs_type_prog :
000340|     runs_type -> state -> execution_ctx -> prog -> result **)
000341|  
000342| let runs_type_prog x = (*[0]*)x.runs_type_prog
000343|  
000344| (** val runs_type_call_full :
000345|     runs_type -> state -> execution_ctx -> object_loc -> value -> value list
000346|     -> result **)
000347|  
000348| let runs_type_call_full x = (*[0]*)x.runs_type_call_full
000349|  
000350| (** val run_object_get_own_prop :
000351|     state -> object_loc -> prop_name -> full_descriptor option **)
000352|  
000353| let run_object_get_own_prop s l x =
000354|   match run_object_method object_get_own_prop_ s l with
000355|   | Coq_builtin_get_own_prop_default ->
000356|     (*[343745]*)let p = run_object_method object_properties_ s l in
000357|     (*[343745]*)if_def_full_descriptor
000358|       (convert_option_attributes (Heap.read_option string_comparable p x))
000359|       (Some Coq_full_descriptor_undef) (fun d -> (*[121922]*)Some d)
000360|   | Coq_builtin_get_own_prop_args_obj -> (*[3]*)(assert false) __
000361|  
000362| (** val object_get_prop_body :
000363|     (state -> value -> prop_name -> full_descriptor option) -> state -> value
000364|     -> prop_name -> full_descriptor option **)
000365|  
000366| let object_get_prop_body run_object_get_prop0 s v x =
000367|   match v with
000368|   | Coq_value_prim w ->
000369|     (*[70517]*)if value_comparable v (Coq_value_prim Coq_prim_null)
000370|     then (*[70517]*)Some Coq_full_descriptor_undef
000371|     else (*[0]*)None
000372|   | Coq_value_object l ->
000373|     (*[150589]*)if_def_full_descriptor (run_object_get_own_prop s l x) None (fun d ->
000374|       (*[150589]*)if full_descriptor_comparable d Coq_full_descriptor_undef
000375|       then (*[91083]*)let lproto = run_object_method object_proto_ s l in
000376|            (*[91083]*)run_object_get_prop0 s lproto x
000377|       else (*[59506]*)Some d)
000378|  
000379| (** val run_object_get_prop :
000380|     state -> value -> prop_name -> full_descriptor option **)
000381|  
000382| let run_object_get_prop x x0 x1 =
000383|   (*[130023]*)(fun bigf -> (*[130023]*)let rec f x = (*[221106]*)bigf f x in (*[130023]*)f) (fun f' p ->
000384|     (*[221106]*)let (p0, x3) = p in
000385|     (*[221106]*)let (x2, x4) = p0 in
000386|     (*[221106]*)object_get_prop_body (fun x5 x6 x7 -> (*[91083]*)f' ((x5, x6), x7)) x2 x4 x3) ((x,
000387|     x0), x1)
000388|  
000389| (** val object_has_prop : state -> object_loc -> prop_name -> bool option **)
000390|  
000391| let object_has_prop s l x =
000392|   (*[95434]*)option_map (fun d ->
000393|     (*[95434]*)neg_decidable (full_descriptor_comparable d Coq_full_descriptor_undef))
000394|     (run_object_get_prop s (Coq_value_object l) x)
000395|  
000396| (** val object_proto_is_prototype_of_body :
000397|     (state -> object_loc -> object_loc -> result) -> state -> object_loc ->
000398|     object_loc -> result **)
000399|  
000400| let object_proto_is_prototype_of_body run_object_proto_is_prototype_of0 s l0 l =
000401|   match run_object_method object_proto_ s l with
000402|   | Coq_value_prim p ->
000403|     (match p with
000404|      | Coq_prim_null ->
000405|        (*[31]*)Coq_result_out (Coq_out_ter (s,
000406|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000407|            false))))))
000408|      | _ ->
000409|        (*[0]*)stuck_heap s
000410|          ('['::('r'::('u'::('n'::('_'::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('m'::('e'::('t'::('h'::('o'::('d'::(']'::(' '::('r'::('e'::('t'::('u'::('r'::('n'::('e'::('d'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(' '::('i'::('n'::(' '::('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('p'::('r'::('o'::('t'::('o'::('_'::('i'::('s'::('_'::('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::('_'::('o'::('f'::('_'::('b'::('o'::('d'::('y'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000411|   | Coq_value_object l' ->
000412|     (*[55]*)if object_loc_comparable l' l0
000413|     then (*[0]*)Coq_result_out (Coq_out_ter (s,
000414|            (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000415|              true))))))
000416|     else (*[55]*)run_object_proto_is_prototype_of0 s l0 l'
000417|  
000418| (** val run_object_proto_is_prototype_of :
000419|     state -> object_loc -> object_loc -> result **)
000420|  
000421| let run_object_proto_is_prototype_of x x0 x1 =
000422|   (*[31]*)(fun bigf -> (*[31]*)let rec f x = (*[86]*)bigf f x in (*[31]*)f) (fun f' p ->
000423|     (*[86]*)let (p0, x3) = p in
000424|     (*[86]*)let (x2, x4) = p0 in
000425|     (*[86]*)object_proto_is_prototype_of_body (fun x5 x6 x7 -> (*[55]*)f' ((x5, x6), x7)) x2
000426|       x4 x3) ((x, x0), x1)
000427|  
000428| (** val env_record_lookup :
000429|     'a1 -> state -> env_loc -> (env_record -> 'a1) -> 'a1 **)
000430|  
000431| let env_record_lookup d s l k =
000432|   (*[94217]*)morph_option d k
000433|     (Heap.read_option nat_comparable s.state_env_record_heap l)
000434|  
000435| (** val env_record_has_binding :
000436|     state -> env_loc -> prop_name -> bool option **)
000437|  
000438| let env_record_has_binding s l x =
000439|   (*[73290]*)env_record_lookup (fun x0 -> (*[0]*)None) s l (fun e x0 ->
000440|     match e with
000441|     | Coq_env_record_decl ed ->
000442|       (*[11833]*)Some (Heap.indom_decidable string_comparable ed x)
000443|     | Coq_env_record_object (l0, pt) -> (*[61457]*)object_has_prop s l0 x) ()
000444|  
000445| (** val lexical_env_get_identifier_ref :
000446|     state -> lexical_env -> prop_name -> strictness_flag -> ref option **)
000447|  
000448| let rec lexical_env_get_identifier_ref s x x0 str =
000449|   match x with
000450|   | [] -> (*[14868]*)Some (ref_create_value (Coq_value_prim Coq_prim_undef) x0 str)
000451|   | l :: x' ->
000452|     (*[44888]*)if_bool_option None (env_record_has_binding s l x0) (fun x1 -> (*[24824]*)Some
000453|       (ref_create_env_loc l x0 str)) (fun x1 ->
000454|       (*[20064]*)lexical_env_get_identifier_ref s x' x0 str)
000455|  
000456| (** val object_delete :
000457|     state -> object_loc -> prop_name -> strictness_flag -> result **)
000458|  
000459| let object_delete s l x str =
000460|   (*[80]*)if_some (run_object_get_own_prop s l x) (fun d ->
000461|     match d with
000462|     | Coq_full_descriptor_undef ->
000463|       (*[10]*)Coq_result_out (Coq_out_ter (s,
000464|         (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool true))))))
000465|     | Coq_full_descriptor_some a ->
000466|       (*[58]*)if attributes_configurable a
000467|       then (*[34]*)Coq_result_out (Coq_out_ter
000468|              ((object_heap_map_properties_pickable s l (fun p ->
000469|                 (*[34]*)Heap.rem string_comparable p x)),
000470|              (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000471|                true))))))
000472|       else (*[24]*)Coq_result_out
000473|              (out_error_or_cst s str (Coq_resvalue_value (Coq_value_object
000474|                (Coq_object_loc_prealloc (Coq_prealloc_native_error
000475|                Coq_native_error_type))))
000476|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000477|                  false))))))
000478|  
000479| (** val env_record_delete_binding :
000480|     state -> env_loc -> prop_name -> result **)
000481|  
000482| let env_record_delete_binding s l x =
000483|   (*[49]*)let e = env_record_binds_pickable s l in
000484|   (match e with
000485|    | Coq_env_record_decl ed ->
000486|      (match Heap.read_option string_comparable ed x with
000487|       | Some p ->
000488|         (*[6]*)let (mu, v) = p in
000489|         (match mu with
000490|          | Coq_mutability_deletable ->
000491|            (*[0]*)let s' =
000492|              env_record_write s l (Coq_env_record_decl
000493|                (decl_env_record_rem ed x))
000494|            in
000495|            (*[0]*)Coq_result_out (Coq_out_ter (s',
000496|            (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000497|              true))))))
000498|          | _ ->
000499|            (*[6]*)Coq_result_out (Coq_out_ter (s,
000500|              (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000501|                false)))))))
000502|       | None ->
000503|         (*[0]*)Coq_result_out (Coq_out_ter (s,
000504|           (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000505|             true)))))))
000506|    | Coq_env_record_object (l0, pt) -> (*[43]*)object_delete s l0 x throw_false)
000507|  
000508| (** val env_record_implicit_this_value : state -> env_loc -> value **)
000509|  
000510| let env_record_implicit_this_value s l =
000511|   match env_record_binds_pickable s l with
000512|   | Coq_env_record_decl ed -> (*[41]*)Coq_value_prim Coq_prim_undef
000513|   | Coq_env_record_object (l0, provide_this) ->
000514|     (*[2491]*)if provide_this
000515|     then (*[0]*)Coq_value_object l0
000516|     else (*[2491]*)Coq_value_prim Coq_prim_undef
000517|  
000518| (** val identifier_res :
000519|     state -> execution_ctx -> prop_name -> ref option **)
000520|  
000521| let identifier_res s c x =
000522|   (*[39692]*)let x0 = c.execution_ctx_lexical_env in
000523|   (*[39692]*)let str = c.execution_ctx_strict in
000524|   (*[39692]*)lexical_env_get_identifier_ref s x0 x str
000525|  
000526| (** val object_get_builtin :
000527|     runs_type -> builtin_get -> state -> execution_ctx -> value -> object_loc
000528|     -> prop_name -> result **)
000529|  
000530| let object_get_builtin runs0 b s c vthis l x =
000531|   match b with
000532|   | Coq_builtin_get_default ->
000533|     (*[25796]*)if_some (run_object_get_prop s (Coq_value_object l) x) (fun d ->
000534|       match d with
000535|       | Coq_full_descriptor_undef ->
000536|         (*[6665]*)Coq_result_out (Coq_out_ter (s,
000537|           (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef)))))
000538|       | Coq_full_descriptor_some a ->
000539|         (match a with
000540|          | Coq_attributes_data_of ad ->
000541|            (*[19130]*)Coq_result_out (Coq_out_ter (s,
000542|              (res_ref (Coq_resvalue_value ad.attributes_data_value))))
000543|          | Coq_attributes_accessor_of aa ->
000544|            (match aa.attributes_accessor_get with
000545|             | Coq_value_prim p ->
000546|               (match p with
000547|                | Coq_prim_undef ->
000548|                  (*[0]*)Coq_result_out (Coq_out_ter (s,
000549|                    (res_ref (Coq_resvalue_value (Coq_value_prim
000550|                      Coq_prim_undef)))))
000551|                | _ ->
000552|                  (*[0]*)stuck_heap s
000553|                    ('W'::('a'::('i'::('t'::('i'::('n'::('g'::(' '::('f'::('o'::('r'::(' '::('s'::('p'::('e'::('c'::('i'::('f'::('i'::('c'::('a'::('t'::('i'::('o'::('n'::(' '::('i'::('n'::(' '::('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('g'::('e'::('t'::('_'::('b'::('u'::('i'::('l'::('t'::('i'::('n'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))
000554|             | Coq_value_object lf ->
000555|               (match vthis with
000556|                | Coq_value_prim p ->
000557|                  (*[0]*)stuck_heap s
000558|                    ('T'::('h'::('e'::(' '::('`'::('t'::('h'::('i'::('s'::('\''::(' '::('a'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::(' '::('o'::('f'::(' '::('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('g'::('e'::('t'::('_'::('b'::('u'::('i'::('l'::('t'::('i'::('n'::(']'::(' '::('i'::('s'::(' '::('a'::(' '::('p'::('r'::('m'::('i'::('t'::('i'::('v'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000559|                | Coq_value_object lthis ->
000560|                  (*[1]*)runs0.runs_type_call_full s c lf (Coq_value_object lthis) []))))
000561|   | _ -> (*[5]*)(assert false) __
000562|  
000563| (** val object_get :
000564|     runs_type -> state -> execution_ctx -> value -> prop_name -> result **)
000565|  
000566| let object_get runs0 s c v x =
000567|   match v with
000568|   | Coq_value_prim p ->
000569|     (*[0]*)stuck_heap s
000570|       ('C'::('a'::('l'::('l'::('i'::('n'::('g'::(' '::('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('g'::('e'::('t'::(']'::(' '::('o'::('n'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))
000571|   | Coq_value_object l ->
000572|     (*[25891]*)let b = run_object_method object_get_ s l in
000573|     (*[25801]*)object_get_builtin runs0 b s c (Coq_value_object l) l x
000574|  
000575| (** val prim_new_object : state -> prim -> result **)
000576|  
000577| let prim_new_object s w =
000578|   (*[116]*)(assert false) __
000579|  
000580| (** val to_object : state -> value -> result **)
000581|  
000582| let to_object s = function
000583| | Coq_value_prim w ->
000584|   (match w with
000585|    | Coq_prim_undef -> (*[0]*)run_error s Coq_native_error_type
000586|    | Coq_prim_null -> (*[0]*)run_error s Coq_native_error_type
000587|    | _ -> (*[116]*)prim_new_object s w)
000588| | Coq_value_object l ->
000589|   (*[608]*)Coq_result_out (Coq_out_ter (s,
000590|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
000591|  
000592| (** val prim_value_get :
000593|     runs_type -> state -> execution_ctx -> value -> prop_name -> result **)
000594|  
000595| let prim_value_get runs0 s c v x =
000596|   (*[64]*)if_object (to_object s v) (fun s' l ->
000597|     (*[0]*)object_get_builtin runs0 Coq_builtin_get_default s' c v l x)
000598|  
000599| (** val run_value_viewable_as_prim :
000600|     char list -> state -> value -> prim option **)
000601|  
000602| let run_value_viewable_as_prim s s0 = function
000603| | Coq_value_prim w -> (*[0]*)Some w
000604| | Coq_value_object l ->
000605|   (match run_object_method object_prim_value_ s0 l with
000606|    | Some v0 ->
000607|      (match v0 with
000608|       | Coq_value_prim w -> (*[0]*)Some w
000609|       | Coq_value_object o -> (*[0]*)None)
000610|    | None -> (*[0]*)None)
000611|  
000612| (** val env_record_get_binding_value :
000613|     runs_type -> state -> execution_ctx -> env_loc -> prop_name ->
000614|     strictness_flag -> result **)
000615|  
000616| let env_record_get_binding_value runs0 s c l x str =
000617|   (*[20927]*)env_record_lookup (fun x0 ->
000618|     (*[0]*)stuck_heap s
000619|       ('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('l'::('o'::('o'::('k'::('u'::('p'::(']'::(' '::('f'::('a'::('i'::('l'::('e'::('d'::(' '::('i'::('n'::(' '::('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('g'::('e'::('t'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000620|     s l (fun er x0 ->
000621|     match er with
000622|     | Coq_env_record_decl ed ->
000623|       (*[2512]*)if_some (Heap.read_option string_comparable ed x) (fun rm ->
000624|         (*[2512]*)let (mu, v) = rm in
000625|         (*[2512]*)if mutability_comparable mu Coq_mutability_uninitialized_immutable
000626|         then (*[0]*)Coq_result_out
000627|                (out_error_or_cst s str (Coq_resvalue_value (Coq_value_object
000628|                  (Coq_object_loc_prealloc (Coq_prealloc_native_error
000629|                  Coq_native_error_ref))))
000630|                  (res_ref (Coq_resvalue_value (Coq_value_prim
000631|                    Coq_prim_undef))))
000632|         else (*[2512]*)Coq_result_out (Coq_out_ter (s,
000633|                (res_ref (Coq_resvalue_value v)))))
000634|     | Coq_env_record_object (l0, pt) ->
000635|       (*[18415]*)if_bool_option_result (object_has_prop s l0 x) (fun x1 ->
000636|         (*[17541]*)object_get runs0 s c (Coq_value_object l0) x) (fun x1 ->
000637|         (*[874]*)Coq_result_out
000638|         (out_error_or_cst s str (Coq_resvalue_value (Coq_value_object
000639|           (Coq_object_loc_prealloc (Coq_prealloc_native_error
000640|           Coq_native_error_ref))))
000641|           (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef))))))
000642|     ()
000643|  
000644| (** val object_can_put : state -> object_loc -> prop_name -> bool option **)
000645|  
000646| let object_can_put s l x =
000647|   (*[29419]*)if_def_full_descriptor (run_object_get_own_prop s l x) None (fun d ->
000648|     match d with
000649|     | Coq_full_descriptor_undef ->
000650|       (match run_object_method object_proto_ s l with
000651|        | Coq_value_prim p ->
000652|          (match p with
000653|           | Coq_prim_null -> (*[8469]*)Some (run_object_method object_extensible_ s l)
000654|           | _ -> (*[0]*)None)
000655|        | Coq_value_object lproto ->
000656|          (*[155]*)option_map (fun d' ->
000657|            match d' with
000658|            | Coq_full_descriptor_undef ->
000659|              (*[137]*)run_object_method object_extensible_ s l
000660|            | Coq_full_descriptor_some a ->
000661|              (match a with
000662|               | Coq_attributes_data_of ad ->
000663|                 (*[18]*)if run_object_method object_extensible_ s l
000664|                 then (*[18]*)ad.attributes_data_writable
000665|                 else (*[0]*)false
000666|               | Coq_attributes_accessor_of aa ->
000667|                 (*[0]*)neg_decidable
000668|                   (value_comparable aa.attributes_accessor_set
000669|                     (Coq_value_prim Coq_prim_undef))))
000670|            (run_object_get_prop s (Coq_value_object lproto) x))
000671|     | Coq_full_descriptor_some a ->
000672|       (match a with
000673|        | Coq_attributes_data_of ad -> (*[20792]*)Some ad.attributes_data_writable
000674|        | Coq_attributes_accessor_of aa ->
000675|          (*[3]*)Some
000676|            (neg_decidable
000677|              (value_comparable aa.attributes_accessor_set (Coq_value_prim
000678|                Coq_prim_undef)))))
000679|  
000680| (** val object_define_own_prop :
000681|     state -> object_loc -> prop_name -> descriptor -> strictness_flag ->
000682|     result **)
000683|  
000684| let object_define_own_prop s l x desc str =
000685|   (*[137608]*)let b = run_object_method object_define_own_prop_ s l in
000686|   (match b with
000687|    | Coq_builtin_define_own_prop_default ->
000688|      (*[134262]*)if_some (run_object_get_own_prop s l x) (fun d ->
000689|        (*[134262]*)let reject = fun s0 ->
000690|          (*[0]*)out_error_or_cst s0 str (Coq_resvalue_value (Coq_value_object
000691|            (Coq_object_loc_prealloc (Coq_prealloc_native_error
000692|            Coq_native_error_type))))
000693|            (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000694|              false))))
000695|        in
000696|        (match d with
000697|         | Coq_full_descriptor_undef ->
000698|           (*[113482]*)if run_object_method object_extensible_ s l
000699|           then (*[113482]*)let a =
000700|                  if or_decidable (descriptor_is_generic_dec desc)
000701|                       (descriptor_is_data_dec desc)
000702|                  then (*[109228]*)Coq_attributes_data_of
000703|                         (attributes_data_of_descriptor desc)
000704|                  else (*[4254]*)Coq_attributes_accessor_of
000705|                         (attributes_accessor_of_descriptor desc)
000706|                in
000707|                (*[113482]*)let s1 = object_set_property_pickable s l x a in
000708|                (*[113482]*)Coq_result_out (Coq_out_ter (s1,
000709|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000710|                  true))))))
000711|           else (*[0]*)Coq_result_out (reject s)
000712|         | Coq_full_descriptor_some a ->
000713|           (*[20780]*)let object_define_own_prop_write = fun s0 a0 ->
000714|             (*[16901]*)let a' = attributes_update a0 desc in
000715|             (*[16901]*)let s' = object_set_property_pickable s0 l x a' in
000716|             (*[16901]*)Coq_out_ter (s',
000717|             (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000718|               true)))))
000719|           in
000720|           (*[20780]*)if descriptor_contains_dec (descriptor_of_attributes a) desc
000721|           then (*[3879]*)Coq_result_out (Coq_out_ter (s,
000722|                  (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
000723|                    true))))))
000724|           else (*[16901]*)if attributes_change_enumerable_on_non_configurable_dec a desc
000725|                then (*[0]*)Coq_result_out (reject s)
000726|                else (*[16901]*)if descriptor_is_generic_dec desc
000727|                     then (*[0]*)Coq_result_out (object_define_own_prop_write s a)
000728|                     else (*[16901]*)if neg_decidable
000729|                               (eq_prop_dec (attributes_is_data_dec a)
000730|                                 (descriptor_is_data_dec desc))
000731|                          then (*[0]*)if neg (attributes_configurable a)
000732|                               then (*[0]*)Coq_result_out (reject s)
000733|                               else (*[0]*)let a' =
000734|                                      match a with
000735|                                      | Coq_attributes_data_of ad ->
000736|                                        (*[0]*)Coq_attributes_accessor_of
000737|                                          (attributes_accessor_of_attributes_data
000738|                                            ad)
000739|                                      | Coq_attributes_accessor_of aa ->
000740|                                        (*[0]*)Coq_attributes_data_of
000741|                                          (attributes_data_of_attributes_accessor
000742|                                            aa)
000743|                                    in
000744|                                    (*[0]*)let s' =
000745|                                      object_set_property_pickable s l x a'
000746|                                    in
000747|                                    (*[0]*)Coq_result_out
000748|                                    (object_define_own_prop_write s' a')
000749|                          else (match a with
000750|                                | Coq_attributes_data_of ad ->
000751|                                  (*[16901]*)if attributes_change_data_on_non_configurable_dec
000752|                                       ad desc
000753|                                  then (*[0]*)Coq_result_out (reject s)
000754|                                  else (*[16901]*)Coq_result_out
000755|                                         (object_define_own_prop_write s a)
000756|                                | Coq_attributes_accessor_of aa ->
000757|                                  (*[0]*)if attributes_change_accessor_on_non_configurable_dec
000758|                                       aa desc
000759|                                  then (*[0]*)Coq_result_out (reject s)
000760|                                  else (*[0]*)Coq_result_out
000761|                                         (object_define_own_prop_write s a))))
000762|    | Coq_builtin_define_own_prop_args_obj ->
000763|      (*[3346]*)Coq_result_out (Coq_out_ter (s,
000764|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool true)))))))
000765|  
000766| (** val ref_get_value :
000767|     runs_type -> state -> execution_ctx -> resvalue -> result **)
000768|  
000769| let ref_get_value runs0 s c = function
000770| | Coq_resvalue_empty ->
000771|   (*[0]*)stuck_heap s
000772|     ('['::('r'::('e'::('f'::('_'::('g'::('e'::('t'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('a'::('n'::(' '::('e'::('m'::('p'::('t'::('y'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::('.'::[])))))))))))))))))))))))))))))))))))))))))
000773| | Coq_resvalue_value v ->
000774|   (*[102346]*)Coq_result_out (Coq_out_ter (s, (res_ref (Coq_resvalue_value v))))
000775| | Coq_resvalue_ref r ->
000776|   (match ref_kind_of r with
000777|    | Coq_ref_kind_primitive_base ->
000778|      (match r.ref_base with
000779|       | Coq_ref_base_type_value v ->
000780|         (*[64]*)if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_primitive_base
000781|         then (*[64]*)prim_value_get runs0 s c v r.ref_name
000782|         else (*[0]*)object_get runs0 s c v r.ref_name
000783|       | Coq_ref_base_type_env_loc l ->
000784|         (*[0]*)env_record_get_binding_value runs0 s c l r.ref_name r.ref_strict)
000785|    | Coq_ref_kind_object ->
000786|      (match r.ref_base with
000787|       | Coq_ref_base_type_value v ->
000788|         (*[7574]*)if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_primitive_base
000789|         then (*[0]*)prim_value_get runs0 s c v r.ref_name
000790|         else (*[7574]*)object_get runs0 s c v r.ref_name
000791|       | Coq_ref_base_type_env_loc l ->
000792|         (*[0]*)env_record_get_binding_value runs0 s c l r.ref_name r.ref_strict)
000793|    | Coq_ref_kind_env_record ->
000794|      (match r.ref_base with
000795|       | Coq_ref_base_type_value v ->
000796|         (*[0]*)stuck_heap s
000797|           ('['::('r'::('e'::('f'::('_'::('g'::('e'::('t'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('a'::(' '::('r'::('e'::('f'::('e'::('r'::('e'::('n'::('c'::('e'::(' '::('t'::('o'::(' '::('a'::('n'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('r'::('e'::('c'::('o'::('r'::('d'::(' '::('w'::('h'::('o'::('s'::('e'::(' '::('b'::('a'::('s'::('e'::(' '::('t'::('y'::('p'::('e'::(' '::('i'::('s'::(' '::('a'::(' '::('v'::('a'::('l'::('u'::('e'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000798|       | Coq_ref_base_type_env_loc l ->
000799|         (*[20927]*)env_record_get_binding_value runs0 s c l r.ref_name r.ref_strict)
000800|    | _ -> (*[6125]*)run_error s Coq_native_error_ref)
000801|  
000802| (** val object_put_complete :
000803|     runs_type -> state -> execution_ctx -> value -> object_loc -> prop_name
000804|     -> value -> strictness_flag -> result_void **)
000805|  
000806| let object_put_complete runs0 s c vthis l x v str =
000807|   (*[29419]*)if_some (object_can_put s l x) (fun b ->
000808|     (*[29419]*)if b
000809|     then (*[29407]*)if_some (run_object_get_own_prop s l x) (fun d ->
000810|            match d with
000811|            | Coq_full_descriptor_undef ->
000812|              (*[8624]*)if_some (run_object_get_prop s (Coq_value_object l) x)
000813|                (fun d' ->
000814|                match d' with
000815|                | Coq_full_descriptor_undef ->
000816|                  (match vthis with
000817|                   | Coq_value_prim wthis ->
000818|                     (*[0]*)Coq_result_out
000819|                       (out_error_or_void s str (Coq_resvalue_value
000820|                         (Coq_value_object (Coq_object_loc_prealloc
000821|                         (Coq_prealloc_native_error Coq_native_error_type)))))
000822|                   | Coq_value_object lthis ->
000823|                     (*[8606]*)let desc = descriptor_intro_data v true true true in
000824|                     (*[8606]*)if_success (object_define_own_prop s l x desc str)
000825|                       (fun s1 rv -> (*[8606]*)Coq_result_out (out_void s1)))
000826|                | Coq_full_descriptor_some a ->
000827|                  (match a with
000828|                   | Coq_attributes_data_of a0 ->
000829|                     (match vthis with
000830|                      | Coq_value_prim wthis ->
000831|                        (*[0]*)Coq_result_out
000832|                          (out_error_or_void s str (Coq_resvalue_value
000833|                            (Coq_value_object (Coq_object_loc_prealloc
000834|                            (Coq_prealloc_native_error
000835|                            Coq_native_error_type)))))
000836|                      | Coq_value_object lthis ->
000837|                        (*[18]*)let desc = descriptor_intro_data v true true true in
000838|                        (*[18]*)if_success (object_define_own_prop s l x desc str)
000839|                          (fun s1 rv -> (*[18]*)Coq_result_out (out_void s1)))
000840|                   | Coq_attributes_accessor_of aa' ->
000841|                     (match aa'.attributes_accessor_set with
000842|                      | Coq_value_prim p ->
000843|                        (*[0]*)stuck_heap s
000844|                          ('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('p'::('u'::('t'::('_'::('c'::('o'::('m'::('p'::('l'::('e'::('t'::('e'::(']'::(' '::('f'::('o'::('u'::('n'::('d'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(' '::('i'::('n'::(' '::('a'::('n'::(' '::('`'::('s'::('e'::('t'::('\''::(' '::('a'::('c'::('c'::('e'::('s'::('s'::('o'::('r'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000845|                      | Coq_value_object lfsetter ->
000846|                        (*[0]*)if_success
000847|                          (runs0.runs_type_call_full s c lfsetter vthis
000848|                            (v :: [])) (fun s1 rv -> (*[0]*)Coq_result_out
000849|                          (out_void s1)))))
000850|            | Coq_full_descriptor_some a ->
000851|              (match a with
000852|               | Coq_attributes_data_of ad ->
000853|                 (match vthis with
000854|                  | Coq_value_prim wthis ->
000855|                    (*[0]*)Coq_result_out
000856|                      (out_error_or_void s str (Coq_resvalue_value
000857|                        (Coq_value_object (Coq_object_loc_prealloc
000858|                        (Coq_prealloc_native_error Coq_native_error_type)))))
000859|                  | Coq_value_object lthis ->
000860|                    (*[20780]*)let desc = { descriptor_value = (Some v);
000861|                      descriptor_writable = None; descriptor_get = None;
000862|                      descriptor_set = None; descriptor_enumerable = None;
000863|                      descriptor_configurable = None }
000864|                    in
000865|                    (*[20780]*)if_success (object_define_own_prop s l x desc str)
000866|                      (fun s1 rv -> (*[20780]*)Coq_result_out (out_void s1)))
000867|               | Coq_attributes_accessor_of a0 ->
000868|                 (*[3]*)if_some (run_object_get_prop s (Coq_value_object l) x)
000869|                   (fun d' ->
000870|                   match d' with
000871|                   | Coq_full_descriptor_undef ->
000872|                     (match vthis with
000873|                      | Coq_value_prim wthis ->
000874|                        (*[0]*)Coq_result_out
000875|                          (out_error_or_void s str (Coq_resvalue_value
000876|                            (Coq_value_object (Coq_object_loc_prealloc
000877|                            (Coq_prealloc_native_error
000878|                            Coq_native_error_type)))))
000879|                      | Coq_value_object lthis ->
000880|                        (*[0]*)let desc = descriptor_intro_data v true true true in
000881|                        (*[0]*)if_success (object_define_own_prop s l x desc str)
000882|                          (fun s1 rv -> (*[0]*)Coq_result_out (out_void s1)))
000883|                   | Coq_full_descriptor_some a1 ->
000884|                     (match a1 with
000885|                      | Coq_attributes_data_of a2 ->
000886|                        (match vthis with
000887|                         | Coq_value_prim wthis ->
000888|                           (*[0]*)Coq_result_out
000889|                             (out_error_or_void s str (Coq_resvalue_value
000890|                               (Coq_value_object (Coq_object_loc_prealloc
000891|                               (Coq_prealloc_native_error
000892|                               Coq_native_error_type)))))
000893|                         | Coq_value_object lthis ->
000894|                           (*[0]*)let desc = descriptor_intro_data v true true true
000895|                           in
000896|                           (*[0]*)if_success (object_define_own_prop s l x desc str)
000897|                             (fun s1 rv -> (*[0]*)Coq_result_out (out_void s1)))
000898|                      | Coq_attributes_accessor_of aa' ->
000899|                        (match aa'.attributes_accessor_set with
000900|                         | Coq_value_prim p ->
000901|                           (*[0]*)stuck_heap s
000902|                             ('['::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('p'::('u'::('t'::('_'::('c'::('o'::('m'::('p'::('l'::('e'::('t'::('e'::(']'::(' '::('f'::('o'::('u'::('n'::('d'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(' '::('i'::('n'::(' '::('a'::('n'::(' '::('`'::('s'::('e'::('t'::('\''::(' '::('a'::('c'::('c'::('e'::('s'::('s'::('o'::('r'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000903|                         | Coq_value_object lfsetter ->
000904|                           (*[3]*)if_success
000905|                             (runs0.runs_type_call_full s c lfsetter vthis
000906|                               (v :: [])) (fun s1 rv -> (*[0]*)Coq_result_out
000907|                             (out_void s1)))))))
000908|     else (*[12]*)Coq_result_out
000909|            (out_error_or_void s str (Coq_resvalue_value (Coq_value_object
000910|              (Coq_object_loc_prealloc (Coq_prealloc_native_error
000911|              Coq_native_error_type))))))
000912|  
000913| (** val object_put :
000914|     runs_type -> state -> execution_ctx -> object_loc -> prop_name -> value
000915|     -> strictness_flag -> result_void **)
000916|  
000917| let object_put runs0 s c l x v str =
000918|   (*[29419]*)object_put_complete runs0 s c (Coq_value_object l) l x v str
000919|  
000920| (** val env_record_set_mutable_binding :
000921|     runs_type -> state -> execution_ctx -> env_loc -> prop_name -> value ->
000922|     strictness_flag -> result_void **)
000923|  
000924| let env_record_set_mutable_binding runs0 s c l x v str =
000925|   match env_record_binds_pickable s l with
000926|   | Coq_env_record_decl ed ->
000927|     (*[5297]*)if_some (Heap.read_option string_comparable ed x) (fun rm ->
000928|       (*[5297]*)let (mu, v_old) = rm in
000929|       (*[5297]*)if neg_decidable (mutability_comparable mu Coq_mutability_immutable)
000930|       then (*[5297]*)Coq_result_out (out_void (env_record_write_decl_env s l x mu v))
000931|       else (*[0]*)if str
000932|            then (*[0]*)run_error s Coq_native_error_type
000933|            else (*[0]*)Coq_result_out (Coq_out_ter (s,
000934|                   (res_ref (Coq_resvalue_value (Coq_value_prim
000935|                     Coq_prim_undef))))))
000936|   | Coq_env_record_object (l0, pt) -> (*[20727]*)object_put runs0 s c l0 x v str
000937|  
000938| (** val prim_value_put :
000939|     runs_type -> state -> execution_ctx -> prim -> prop_name -> value ->
000940|     strictness_flag -> result_void **)
000941|  
000942| let prim_value_put runs0 s c w x v str =
000943|   (*[0]*)if_object (to_object s (Coq_value_prim w)) (fun s1 l ->
000944|     (*[0]*)object_put_complete runs0 s1 c (Coq_value_prim w) l x v str)
000945|  
000946| (** val ref_put_value :
000947|     runs_type -> state -> execution_ctx -> resvalue -> value -> result_void **)
000948|  
000949| let ref_put_value runs0 s c rv v =
000950|   match rv with
000951|   | Coq_resvalue_empty ->
000952|     (*[0]*)stuck_heap s
000953|       ('['::('r'::('e'::('f'::('_'::('p'::('u'::('t'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('a'::('n'::(' '::('e'::('m'::('p'::('t'::('y'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::('.'::[])))))))))))))))))))))))))))))))))))))))))
000954|   | Coq_resvalue_value v0 -> (*[21]*)run_error s Coq_native_error_ref
000955|   | Coq_resvalue_ref r ->
000956|     (*[14021]*)if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_undef
000957|     then (*[8351]*)if r.ref_strict
000958|          then (*[87]*)run_error s Coq_native_error_ref
000959|          else (*[8264]*)object_put runs0 s c (Coq_object_loc_prealloc
000960|                 Coq_prealloc_global) r.ref_name v throw_false
000961|     else (match r.ref_base with
000962|           | Coq_ref_base_type_value v0 ->
000963|             (match v0 with
000964|              | Coq_value_prim w ->
000965|                (*[0]*)if ref_kind_comparable (ref_kind_of r)
000966|                     Coq_ref_kind_primitive_base
000967|                then (*[0]*)prim_value_put runs0 s c w r.ref_name v r.ref_strict
000968|                else (*[0]*)stuck_heap s
000969|                       ('['::('r'::('e'::('f'::('_'::('p'::('u'::('t'::('_'::('v'::('a'::('l'::('u'::('e'::(']'::(' '::('f'::('o'::('u'::('n'::('d'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(' '::('b'::('a'::('s'::('e'::(' '::('w'::('h'::('o'::('s'::('e'::(' '::('k'::('i'::('n'::('d'::(' '::('i'::('s'::(' '::('n'::('o'::('t'::(' '::('a'::(' '::('p'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::('!'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000970|              | Coq_value_object l ->
000971|                (*[428]*)object_put runs0 s c l r.ref_name v r.ref_strict)
000972|           | Coq_ref_base_type_env_loc l ->
000973|             (*[5242]*)env_record_set_mutable_binding runs0 s c l r.ref_name v
000974|               r.ref_strict)
000975|  
000976| (** val if_success_value :
000977|     runs_type -> execution_ctx -> result -> (state -> value -> result) ->
000978|     result **)
000979|  
000980| let if_success_value runs0 c o k =
000981|   (*[140818]*)if_success o (fun s1 rv1 ->
000982|     (*[129875]*)if_success (ref_get_value runs0 s1 c rv1) (fun s2 rv2 ->
000983|       match rv2 with
000984|       | Coq_resvalue_value v -> (*[123590]*)k s2 v
000985|       | _ -> (*[0]*)run_error s2 Coq_native_error_ref))
000986|  
000987| (** val env_record_create_mutable_binding :
000988|     state -> env_loc -> prop_name -> bool option -> result_void **)
000989|  
000990| let env_record_create_mutable_binding s l x deletable_opt =
000991|   (*[20764]*)let deletable = unsome_default false deletable_opt in
000992|   (match env_record_binds_pickable s l with
000993|    | Coq_env_record_decl ed ->
000994|      (*[5219]*)if Heap.indom_decidable string_comparable ed x
000995|      then (*[0]*)stuck_heap s
000996|             ('A'::('l'::('r'::('e'::('a'::('d'::('y'::(' '::('d'::('e'::('c'::('l'::('a'::('r'::('e'::('d'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('r'::('e'::('c'::('o'::('r'::('d'::(' '::('i'::('n'::(' '::('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('c'::('r'::('e'::('a'::('t'::('e'::('_'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
000997|      else (*[5219]*)let s' =
000998|             env_record_write_decl_env s l x (mutability_of_bool deletable)
000999|               (Coq_value_prim Coq_prim_undef)
001000|           in
001001|           (*[5219]*)Coq_result_out (out_void s')
001002|    | Coq_env_record_object (l0, pt) ->
001003|      (*[15545]*)if_bool_option_result (object_has_prop s l0 x) (fun x0 ->
001004|        (*[0]*)stuck_heap s
001005|          ('A'::('l'::('r'::('e'::('a'::('d'::('y'::(' '::('d'::('e'::('c'::('l'::('a'::('r'::('e'::('d'::(' '::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(' '::('i'::('n'::(' '::('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('c'::('r'::('e'::('a'::('t'::('e'::('_'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001006|        (fun x0 ->
001007|        (*[15545]*)let a = { attributes_data_value = (Coq_value_prim Coq_prim_undef);
001008|          attributes_data_writable = true; attributes_data_enumerable = true;
001009|          attributes_data_configurable = deletable }
001010|        in
001011|        (*[15545]*)if_success
001012|          (object_define_own_prop s l0 x
001013|            (descriptor_of_attributes (Coq_attributes_data_of a)) throw_true)
001014|          (fun s1 rv -> (*[15545]*)Coq_result_out (out_void s1))))
001015|  
001016| (** val env_record_create_set_mutable_binding :
001017|     runs_type -> state -> execution_ctx -> env_loc -> prop_name -> bool
001018|     option -> value -> strictness_flag -> result_void **)
001019|  
001020| let env_record_create_set_mutable_binding runs0 s c l x deletable_opt v str =
001021|   (*[7108]*)if_void (env_record_create_mutable_binding s l x deletable_opt) (fun s0 ->
001022|     (*[7108]*)env_record_set_mutable_binding runs0 s0 c l x v str)
001023|  
001024| (** val env_record_create_immutable_binding :
001025|     state -> env_loc -> prop_name -> result_void **)
001026|  
001027| let env_record_create_immutable_binding s l x =
001028|   match env_record_binds_pickable s l with
001029|   | Coq_env_record_decl ed ->
001030|     (*[107]*)if Heap.indom_decidable string_comparable ed x
001031|     then (*[0]*)stuck_heap s
001032|            ('A'::('l'::('r'::('e'::('a'::('d'::('y'::(' '::('d'::('e'::('c'::('l'::('a'::('r'::('e'::('d'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('r'::('e'::('c'::('o'::('r'::('d'::(' '::('i'::('n'::(' '::('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('c'::('r'::('e'::('a'::('t'::('e'::('_'::('i'::('m'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001033|     else (*[107]*)Coq_result_out
001034|            (out_void
001035|              (env_record_write_decl_env s l x
001036|                Coq_mutability_uninitialized_immutable (Coq_value_prim
001037|                Coq_prim_undef)))
001038|   | Coq_env_record_object (o, p) ->
001039|     (*[0]*)stuck_heap s
001040|       ('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('c'::('r'::('e'::('a'::('t'::('e'::('_'::('i'::('m'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('a'::('n'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('r'::('e'::('c'::('o'::('r'::('d'::(' '::('o'::('b'::('j'::('e'::('c'::('t'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001041|  
001042| (** val env_record_initialize_immutable_binding :
001043|     state -> env_loc -> prop_name -> value -> result_void **)
001044|  
001045| let env_record_initialize_immutable_binding s l x v =
001046|   match env_record_binds_pickable s l with
001047|   | Coq_env_record_decl ed ->
001048|     (*[107]*)if prod_comparable mutability_comparable value_comparable
001049|          (decl_env_record_pickable ed x)
001050|          (Coq_mutability_uninitialized_immutable, (Coq_value_prim
001051|          Coq_prim_undef))
001052|     then (*[107]*)let s' = env_record_write_decl_env s l x Coq_mutability_immutable v
001053|          in
001054|          (*[107]*)Coq_result_out (out_void s')
001055|     else (*[0]*)stuck_heap s
001056|            ('N'::('o'::('n'::(' '::('s'::('u'::('i'::('t'::('a'::('b'::('l'::('e'::(' '::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(' '::('i'::('n'::(' '::('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('i'::('n'::('i'::('t'::('i'::('a'::('l'::('i'::('z'::('e'::('_'::('i'::('m'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001057|   | Coq_env_record_object (o, p) ->
001058|     (*[0]*)stuck_heap s
001059|       ('['::('e'::('n'::('v'::('_'::('r'::('e'::('c'::('o'::('r'::('d'::('_'::('i'::('n'::('i'::('t'::('i'::('a'::('l'::('i'::('z'::('e'::('_'::('i'::('m'::('m'::('u'::('t'::('a'::('b'::('l'::('e'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('a'::('n'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('r'::('e'::('c'::('o'::('r'::('d'::(' '::('o'::('b'::('j'::('e'::('c'::('t'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001060|  
001061| (** val object_default_value :
001062|     runs_type -> state -> execution_ctx -> object_loc -> preftype option ->
001063|     result **)
001064|  
001065| let object_default_value runs0 s c l prefo =
001066|   (*[432]*)let gpref = unsome_default Coq_preftype_number prefo in
001067|   (*[432]*)let lpref = other_preftypes gpref in
001068|   (*[432]*)let gmeth = method_of_preftype gpref in
001069|   (*[432]*)let sub0 = fun s' x k ->
001070|     (*[691]*)if_object (object_get runs0 s' c (Coq_value_object l) x) (fun s1 lfo ->
001071|       (*[691]*)let lf = Coq_value_object lfo in
001072|       (match run_callable s1 lf with
001073|        | Some b ->
001074|          (*[691]*)if_success_value runs0 c
001075|            (runs0.runs_type_call_full s1 c lfo (Coq_value_object l) [])
001076|            (fun s2 v ->
001077|            match v with
001078|            | Coq_value_prim w ->
001079|              (*[350]*)Coq_result_out (Coq_out_ter (s2,
001080|                (res_ref (Coq_resvalue_value (Coq_value_prim w)))))
001081|            | Coq_value_object l0 -> (*[287]*)k s2)
001082|        | None -> (*[0]*)k s1))
001083|   in
001084|   (*[432]*)sub0 s gmeth (fun s' ->
001085|     (*[259]*)let lmeth = method_of_preftype lpref in
001086|     (*[259]*)sub0 s' lmeth (fun s'' -> (*[28]*)run_error s'' Coq_native_error_type))
001087|  
001088| (** val to_primitive :
001089|     runs_type -> state -> execution_ctx -> value -> preftype option -> result **)
001090|  
001091| let to_primitive runs0 s c v prefo =
001092|   match v with
001093|   | Coq_value_prim w ->
001094|     (*[10320]*)Coq_result_out (Coq_out_ter (s,
001095|       (res_ref (Coq_resvalue_value (Coq_value_prim w)))))
001096|   | Coq_value_object l -> (*[432]*)object_default_value runs0 s c l prefo
001097|  
001098| (** val to_number :
001099|     runs_type -> state -> execution_ctx -> value -> result **)
001100|  
001101| let to_number runs0 s c = function
001102| | Coq_value_prim w ->
001103|   (*[23266]*)Coq_result_out (Coq_out_ter (s,
001104|     (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001105|       (convert_prim_to_number w)))))))
001106| | Coq_value_object l ->
001107|   (*[275]*)if_success_primitive
001108|     (to_primitive runs0 s c (Coq_value_object l) (Some Coq_preftype_number))
001109|     (fun s1 w -> (*[227]*)Coq_result_out (Coq_out_ter (s1,
001110|     (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001111|       (convert_prim_to_number w))))))))
001112|  
001113| (** val to_int32 :
001114|     runs_type -> state -> execution_ctx -> value -> (state -> int -> result)
001115|     -> result **)
001116|  
001117| let to_int32 runs0 s c v k =
001118|   (*[6152]*)if_number (to_number runs0 s c v) (fun s' n -> (*[6137]*)k s' (to_int32 n))
001119|  
001120| (** val to_uint32 :
001121|     runs_type -> state -> execution_ctx -> value -> (state -> int -> result)
001122|     -> result **)
001123|  
001124| let to_uint32 runs0 s c v k =
001125|   (*[10306]*)if_number (to_number runs0 s c v) (fun s' n -> (*[10297]*)k s' (to_uint32 n))
001126|  
001127| (** val to_string :
001128|     runs_type -> state -> execution_ctx -> value -> result **)
001129|  
001130| let to_string runs0 s c = function
001131| | Coq_value_prim w ->
001132|   (*[11176]*)Coq_result_out (Coq_out_ter (s,
001133|     (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
001134|       (convert_prim_to_string w)))))))
001135| | Coq_value_object l ->
001136|   (*[0]*)if_success_primitive
001137|     (to_primitive runs0 s c (Coq_value_object l) (Some Coq_preftype_string))
001138|     (fun s1 w -> (*[0]*)Coq_result_out (Coq_out_ter (s1,
001139|     (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
001140|       (convert_prim_to_string w))))))))
001141|  
001142| (** val call_object_new : state -> value -> result **)
001143|  
001144| let call_object_new s v =
001145|   match type_of v with
001146|   | Coq_type_undef ->
001147|     (*[32522]*)let o =
001148|       object_new (Coq_value_object (Coq_object_loc_prealloc
001149|         Coq_prealloc_object_proto))
001150|         ('O'::('b'::('j'::('e'::('c'::('t'::[]))))))
001151|     in
001152|     (*[32522]*)let (l, s') = object_alloc s o in
001153|     (*[32522]*)Coq_result_out (Coq_out_ter (s',
001154|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001155|   | Coq_type_null ->
001156|     (*[3]*)let o =
001157|       object_new (Coq_value_object (Coq_object_loc_prealloc
001158|         Coq_prealloc_object_proto))
001159|         ('O'::('b'::('j'::('e'::('c'::('t'::[]))))))
001160|     in
001161|     (*[3]*)let (l, s') = object_alloc s o in
001162|     (*[3]*)Coq_result_out (Coq_out_ter (s',
001163|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001164|   | Coq_type_object ->
001165|     (*[5]*)Coq_result_out (Coq_out_ter (s, (res_ref (Coq_resvalue_value v))))
001166|   | _ -> (*[33]*)to_object s v
001167|  
001168| (** val bool_proto_value_of_call : state -> execution_ctx -> result **)
001169|  
001170| let bool_proto_value_of_call s c =
001171|   (*[0]*)let v = c.execution_ctx_this_binding in
001172|   (match run_value_viewable_as_prim
001173|            ('B'::('o'::('o'::('l'::('e'::('a'::('n'::[]))))))) s v with
001174|    | Some p ->
001175|      (match p with
001176|       | Coq_prim_bool b ->
001177|         (*[0]*)Coq_result_out (Coq_out_ter (s,
001178|           (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool b))))))
001179|       | _ -> (*[0]*)run_error s Coq_native_error_type)
001180|    | None -> (*[0]*)run_error s Coq_native_error_type)
001181|  
001182| (** val run_construct_prealloc :
001183|     runs_type -> prealloc -> state -> execution_ctx -> value list -> result **)
001184|  
001185| let run_construct_prealloc runs0 b s c args =
001186|   match b with
001187|   | Coq_prealloc_object -> (*[32563]*)let v = get_arg 0 args in (*[32563]*)call_object_new s v
001188|   | Coq_prealloc_function -> (*[54]*)(assert false) __
001189|   | Coq_prealloc_bool ->
001190|     (*[0]*)let v = get_arg 0 args in
001191|     (*[0]*)let b0 = convert_value_to_boolean v in
001192|     (*[0]*)let o1 =
001193|       object_new (Coq_value_object (Coq_object_loc_prealloc
001194|         Coq_prealloc_bool_proto))
001195|         ('B'::('o'::('o'::('l'::('e'::('a'::('n'::[])))))))
001196|     in
001197|     (*[0]*)let o =
001198|       object_with_primitive_value o1 (Coq_value_prim (Coq_prim_bool b0))
001199|     in
001200|     (*[0]*)let (l, s') = object_alloc s o in
001201|     (*[0]*)Coq_result_out (Coq_out_ter (s',
001202|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001203|   | Coq_prealloc_number ->
001204|     (*[0]*)let follow = fun s' v ->
001205|       (*[0]*)let o1 =
001206|         object_new (Coq_value_object (Coq_object_loc_prealloc
001207|           Coq_prealloc_number_proto))
001208|           ('N'::('u'::('m'::('b'::('e'::('r'::[]))))))
001209|       in
001210|       (*[0]*)let o = object_with_primitive_value o1 v in
001211|       (*[0]*)let (l, s1) = object_alloc s' o in
001212|       (*[0]*)Coq_out_ter (s1, (res_ref (Coq_resvalue_value (Coq_value_object l))))
001213|     in
001214|     (*[0]*)if eq_nil_dec args
001215|     then (*[0]*)Coq_result_out (follow s (Coq_value_prim (Coq_prim_number zero)))
001216|     else (*[0]*)let v = get_arg 0 args in
001217|          (*[0]*)if_value (to_number runs0 s c v) (fun s' v0 -> (*[0]*)Coq_result_out
001218|            (follow s' v0))
001219|   | Coq_prealloc_array -> (*[0]*)(assert false) __
001220|   | Coq_prealloc_string -> (*[0]*)(assert false) __
001221|   | _ ->
001222|     (*[7]*)stuck_heap s
001223|       ('M'::('i'::('s'::('s'::('i'::('n'::('g'::(' '::('c'::('a'::('s'::('e'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('c'::('o'::('n'::('s'::('t'::('r'::('u'::('c'::('t'::('_'::('p'::('r'::('e'::('a'::('l'::('l'::('o'::('c'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))
001224|  
001225| (** val run_construct_default :
001226|     runs_type -> state -> execution_ctx -> object_loc -> value list -> result **)
001227|  
001228| let run_construct_default runs0 s c l args =
001229|   (*[83]*)if_value
001230|     (object_get runs0 s c (Coq_value_object l)
001231|       ('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::[]))))))))))
001232|     (fun s1 v1 ->
001233|     (*[83]*)let vproto =
001234|       if type_comparable (type_of v1) Coq_type_object
001235|       then (*[81]*)v1
001236|       else (*[2]*)Coq_value_object (Coq_object_loc_prealloc
001237|              Coq_prealloc_object_proto)
001238|     in
001239|     (*[83]*)let o = object_new vproto ('O'::('b'::('j'::('e'::('c'::('t'::[])))))) in
001240|     (*[83]*)let (l', s2) = object_alloc s1 o in
001241|     (*[83]*)if_value (runs0.runs_type_call_full s2 c l (Coq_value_object l') args)
001242|       (fun s3 v2 ->
001243|       (*[55]*)let vr =
001244|         if type_comparable (type_of v2) Coq_type_object
001245|         then (*[13]*)v2
001246|         else (*[42]*)Coq_value_object l'
001247|       in
001248|       (*[55]*)Coq_result_out (Coq_out_ter (s3, (res_ref (Coq_resvalue_value vr))))))
001249|  
001250| (** val run_construct :
001251|     runs_type -> state -> execution_ctx -> object_loc -> value list -> result **)
001252|  
001253| let run_construct runs0 s c l args =
001254|   (*[279]*)if_some (run_object_method object_construct_ s l) (fun co ->
001255|     match co with
001256|     | Coq_construct_default -> (*[83]*)run_construct_default runs0 s c l args
001257|     | Coq_construct_after_bind ->
001258|       (*[0]*)stuck_heap s
001259|         ('['::('c'::('o'::('n'::('s'::('t'::('r'::('u'::('c'::('t'::('_'::('a'::('f'::('t'::('e'::('r'::('_'::('b'::('i'::('n'::('d'::(']'::(' '::('r'::('e'::('c'::('e'::('i'::('v'::('e'::('d'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('c'::('o'::('n'::('s'::('t'::('r'::('u'::('c'::('t'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))
001260|     | Coq_construct_prealloc b -> (*[196]*)run_construct_prealloc runs0 b s c args)
001261|  
001262| (** val creating_function_object_proto :
001263|     runs_type -> state -> execution_ctx -> object_loc -> result **)
001264|  
001265| let creating_function_object_proto runs0 s c l =
001266|   (*[21184]*)if_object (run_construct_prealloc runs0 Coq_prealloc_object s c [])
001267|     (fun s1 lproto ->
001268|     (*[21184]*)let a1 = { attributes_data_value = (Coq_value_object l);
001269|       attributes_data_writable = true; attributes_data_enumerable = false;
001270|       attributes_data_configurable = true }
001271|     in
001272|     (*[21184]*)if_bool
001273|       (object_define_own_prop s1 lproto
001274|         ('c'::('o'::('n'::('s'::('t'::('r'::('u'::('c'::('t'::('o'::('r'::[])))))))))))
001275|         (descriptor_of_attributes (Coq_attributes_data_of a1)) false)
001276|       (fun s2 b ->
001277|       (*[21184]*)let a2 = { attributes_data_value = (Coq_value_object lproto);
001278|         attributes_data_writable = true; attributes_data_enumerable = false;
001279|         attributes_data_configurable = false }
001280|       in
001281|       (*[21184]*)object_define_own_prop s2 l
001282|         ('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::[])))))))))
001283|         (descriptor_of_attributes (Coq_attributes_data_of a2)) false))
001284|  
001285| (** val creating_function_object :
001286|     runs_type -> state -> execution_ctx -> char list list -> funcbody ->
001287|     lexical_env -> strictness_flag -> result **)
001288|  
001289| let creating_function_object runs0 s c names bd x str =
001290|   (*[21184]*)let o =
001291|     object_create (Coq_value_object (Coq_object_loc_prealloc
001292|       Coq_prealloc_function_proto))
001293|       ('F'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::[])))))))) true
001294|       Heap.empty
001295|   in
001296|   (*[21184]*)let o1 =
001297|     object_with_invokation o (Some Coq_construct_default) (Some
001298|       Coq_call_default) (Some Coq_builtin_has_instance_function)
001299|   in
001300|   (*[21184]*)let o2 =
001301|     object_with_details o1 (Some x) (Some names) (Some bd) None None None
001302|       None
001303|   in
001304|   (*[21184]*)let (l, s1) = object_alloc s o2 in
001305|   (*[21184]*)let a1 = { attributes_data_value = (Coq_value_prim (Coq_prim_number
001306|     (of_int (my_Z_of_nat (length names))))); attributes_data_writable =
001307|     false; attributes_data_enumerable = false; attributes_data_configurable =
001308|     false }
001309|   in
001310|   (*[21184]*)if_success
001311|     (object_define_own_prop s1 l ('l'::('e'::('n'::('g'::('t'::('h'::[]))))))
001312|       (descriptor_of_attributes (Coq_attributes_data_of a1)) false)
001313|     (fun s2 rv1 ->
001314|     (*[21184]*)if_bool (creating_function_object_proto runs0 s2 c l) (fun s3 b ->
001315|       (*[21184]*)if negb str
001316|       then (*[20713]*)Coq_result_out (Coq_out_ter (s3,
001317|              (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001318|       else (*[471]*)let vthrower = Coq_value_object (Coq_object_loc_prealloc
001319|              Coq_prealloc_throw_type_error)
001320|            in
001321|            (*[471]*)let a2 = { attributes_accessor_get = vthrower;
001322|              attributes_accessor_set = vthrower;
001323|              attributes_accessor_enumerable = false;
001324|              attributes_accessor_configurable = false }
001325|            in
001326|            (*[471]*)if_success
001327|              (object_define_own_prop s3 l
001328|                ('c'::('a'::('l'::('l'::('e'::('r'::[]))))))
001329|                (descriptor_of_attributes (Coq_attributes_accessor_of a2))
001330|                false) (fun s4 rv2 ->
001331|              (*[471]*)if_success
001332|                (object_define_own_prop s4 l
001333|                  ('a'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::('s'::[])))))))))
001334|                  (descriptor_of_attributes (Coq_attributes_accessor_of a2))
001335|                  false) (fun s5 rv3 -> (*[471]*)Coq_result_out (Coq_out_ter (s5,
001336|                (res_ref (Coq_resvalue_value (Coq_value_object l)))))))))
001337|  
001338| (** val binding_inst_formal_params :
001339|     runs_type -> state -> execution_ctx -> env_loc -> value list -> char list
001340|     list -> strictness_flag -> result_void **)
001341|  
001342| let rec binding_inst_formal_params runs0 s c l args names str =
001343|   match names with
001344|   | [] -> (*[2555]*)Coq_result_out (out_void s)
001345|   | argname :: names' ->
001346|     (*[1751]*)let v = hd (Coq_value_prim Coq_prim_undef) args in
001347|     (*[1751]*)if_some (env_record_has_binding s l argname) (fun hb ->
001348|       (*[1751]*)let follow = fun s' ->
001349|         (*[1751]*)if_void (env_record_set_mutable_binding runs0 s' c l argname v str)
001350|           (fun s1 ->
001351|           (*[1751]*)binding_inst_formal_params runs0 s1 c l (tl args) names' str)
001352|       in
001353|       (*[1751]*)if hb
001354|       then (*[5]*)follow s
001355|       else (*[1746]*)if_void (env_record_create_mutable_binding s l argname None)
001356|              follow)
001357|  
001358| (** val binding_inst_function_decls :
001359|     runs_type -> state -> execution_ctx -> env_loc -> funcdecl list ->
001360|     strictness_flag -> bool -> result_void **)
001361|  
001362| let rec binding_inst_function_decls runs0 s c l fds str bconfig =
001363|   match fds with
001364|   | [] -> (*[10465]*)Coq_result_out (out_void s)
001365|   | fd :: fds' ->
001366|     (*[11923]*)let fbd = fd.funcdecl_body in
001367|     (*[11923]*)let str_fd = funcbody_is_strict fbd in
001368|     (*[11923]*)let fparams = fd.funcdecl_parameters in
001369|     (*[11923]*)let fname = fd.funcdecl_name in
001370|     (*[11923]*)if_object
001371|       (creating_function_object runs0 s c fparams fbd
001372|         c.execution_ctx_variable_env str_fd) (fun s1 fo ->
001373|       (*[11923]*)let follow = fun s2 ->
001374|         (*[11923]*)if_void
001375|           (env_record_set_mutable_binding runs0 s2 c l fname
001376|             (Coq_value_object fo) str) (fun s3 ->
001377|           (*[11923]*)binding_inst_function_decls runs0 s3 c l fds' str bconfig)
001378|       in
001379|       (*[11923]*)if_bool_option_result (env_record_has_binding s1 l fname) (fun x ->
001380|         (*[13]*)if nat_comparable l env_loc_global_env_record
001381|         then (*[11]*)if_some
001382|                (run_object_get_prop s1 (Coq_value_object
001383|                  (Coq_object_loc_prealloc Coq_prealloc_global)) fname)
001384|                (fun d ->
001385|                match d with
001386|                | Coq_full_descriptor_undef ->
001387|                  (*[0]*)stuck_heap s1
001388|                    ('U'::('n'::('d'::('e'::('f'::('i'::('n'::('e'::('d'::(' '::('f'::('u'::('l'::('l'::(' '::('d'::('e'::('s'::('c'::('r'::('i'::('p'::('t'::('o'::('r'::(' '::('i'::('n'::(' '::('['::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::('_'::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::('_'::('d'::('e'::('c'::('l'::('s'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001389|                | Coq_full_descriptor_some a ->
001390|                  (*[11]*)if istrue_dec (attributes_configurable a)
001391|                  then (*[0]*)let a' = { attributes_data_value = (Coq_value_prim
001392|                         Coq_prim_undef); attributes_data_writable = true;
001393|                         attributes_data_enumerable = true;
001394|                         attributes_data_configurable = bconfig }
001395|                       in
001396|                       (*[0]*)if_void
001397|                         (object_define_own_prop s1 (Coq_object_loc_prealloc
001398|                           Coq_prealloc_global) fname
001399|                           (descriptor_of_attributes (Coq_attributes_data_of
001400|                             a')) true) follow
001401|                  else (*[11]*)if or_decidable
001402|                            (descriptor_is_accessor_dec
001403|                              (descriptor_of_attributes a))
001404|                            (or_decidable
001405|                              (bool_comparable (attributes_writable a) false)
001406|                              (bool_comparable (attributes_enumerable a)
001407|                                false))
001408|                       then (*[0]*)run_error s1 Coq_native_error_type
001409|                       else (*[11]*)follow s1)
001410|         else (*[2]*)follow s1) (fun x ->
001411|         (*[11910]*)if_void (env_record_create_mutable_binding s1 l fname (Some bconfig))
001412|           follow))
001413|  
001414| (** val binding_inst_var_decls :
001415|     runs_type -> state -> execution_ctx -> env_loc -> char list list -> bool
001416|     -> strictness_flag -> result_void **)
001417|  
001418| let rec binding_inst_var_decls runs0 s c l vds bconfig str =
001419|   match vds with
001420|   | [] -> (*[10465]*)Coq_result_out (out_void s)
001421|   | vd :: vds' ->
001422|     (*[4263]*)let bivd = fun s0 -> (*[4263]*)binding_inst_var_decls runs0 s0 c l vds' bconfig str
001423|     in
001424|     (*[4263]*)if_bool_option_result (env_record_has_binding s l vd) (fun x -> (*[518]*)bivd s)
001425|       (fun x ->
001426|       (*[3745]*)if_void
001427|         (env_record_create_set_mutable_binding runs0 s c l vd (Some bconfig)
001428|           (Coq_value_prim Coq_prim_undef) str) (fun s1 -> (*[3745]*)bivd s1))
001429|  
001430| (** val make_arg_getter :
001431|     state -> object_loc -> prop_name -> env_loc -> result **)
001432|  
001433| let make_arg_getter s l x l0 =
001434|   (*[1712]*)Coq_result_out (Coq_out_ter (s,
001435|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001436|  
001437| (** val make_arg_setter :
001438|     state -> object_loc -> prop_name -> env_loc -> result **)
001439|  
001440| let make_arg_setter s l x l0 =
001441|   (*[1712]*)Coq_result_out (Coq_out_ter (s,
001442|     (res_ref (Coq_resvalue_value (Coq_value_object l)))))
001443|  
001444| (** val arguments_object_map_loop :
001445|     state -> object_loc -> char list list -> int -> value list -> env_loc ->
001446|     strictness_flag -> object_loc -> char list list -> result_void **)
001447|  
001448| let rec arguments_object_map_loop s l xs len args l0 str lmap xsmap =
001449|   (*[4402]*)(fun fO fS n -> (*[4402]*)if n=0 then (*[2551]*)fO () else (*[1851]*)fS (n-1))
001450|     (fun _ ->
001451|     (*[2551]*)if eq_nil_dec xsmap
001452|     then (*[878]*)Coq_result_out (out_void s)
001453|     else (*[1673]*)let o = object_binds_pickable s l in
001454|          (*[1673]*)let o' =
001455|            object_for_args_object o lmap Coq_builtin_get_args_obj
001456|              Coq_builtin_get_own_prop_args_obj
001457|              Coq_builtin_define_own_prop_args_obj Coq_builtin_delete_args_obj
001458|          in
001459|          (*[1673]*)Coq_result_out (out_void (object_write s l o')))
001460|     (fun len' ->
001461|     (*[1851]*)let arguments_object_map_loop' = fun s0 xsmap0 ->
001462|       (*[1851]*)arguments_object_map_loop s0 l xs len' (removelast args) l0 str lmap
001463|         xsmap0
001464|     in
001465|     (*[1851]*)let a =
001466|       attributes_data_intro_all_true
001467|         (last args (Coq_value_prim Coq_prim_undef))
001468|     in
001469|     (*[1851]*)if_bool
001470|       (object_define_own_prop s l
001471|         (convert_prim_to_string (Coq_prim_number
001472|           (of_int (my_Z_of_nat len'))))
001473|         (descriptor_of_attributes (Coq_attributes_data_of a)) false)
001474|       (fun s1 b ->
001475|       (*[1851]*)if ge_nat_decidable len' (length xs)
001476|       then (*[135]*)arguments_object_map_loop' s1 xsmap
001477|       else (*[1716]*)let x = nth len' xs [] in
001478|            (*[1716]*)if or_decidable (bool_comparable str true)
001479|                 (coq_In_decidable string_comparable x xsmap)
001480|            then (*[4]*)arguments_object_map_loop' s1 xsmap
001481|            else (*[1712]*)if_object (make_arg_getter s1 l x l0) (fun s2 lgetter ->
001482|                   (*[1712]*)if_object (make_arg_setter s2 l x l0) (fun s3 lsetter ->
001483|                     (*[1712]*)let a' = { attributes_accessor_get = (Coq_value_object
001484|                       lgetter); attributes_accessor_set = (Coq_value_object
001485|                       lsetter); attributes_accessor_enumerable = false;
001486|                       attributes_accessor_configurable = true }
001487|                     in
001488|                     (*[1712]*)if_bool
001489|                       (object_define_own_prop s3 lmap
001490|                         (convert_prim_to_string (Coq_prim_number
001491|                           (of_int (my_Z_of_nat len'))))
001492|                         (descriptor_of_attributes (Coq_attributes_accessor_of
001493|                           a')) false) (fun s4 b' ->
001494|                       (*[1712]*)arguments_object_map_loop' s4 (x :: xsmap))))))
001495|     len
001496|  
001497| (** val arguments_object_map :
001498|     runs_type -> state -> execution_ctx -> object_loc -> char list list ->
001499|     value list -> env_loc -> strictness_flag -> result_void **)
001500|  
001501| let arguments_object_map runs0 s c l xs args l0 str =
001502|   (*[2551]*)if_object (run_construct_prealloc runs0 Coq_prealloc_object s c [])
001503|     (fun s' lmap ->
001504|     (*[2551]*)arguments_object_map_loop s' l xs (length args) args l0 str lmap [])
001505|  
001506| (** val create_arguments_object :
001507|     runs_type -> state -> execution_ctx -> object_loc -> char list list ->
001508|     value list -> env_loc -> strictness_flag -> result **)
001509|  
001510| let create_arguments_object runs0 s c lf xs args l str =
001511|   (*[2551]*)let o =
001512|     object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
001513|       Coq_prealloc_object_proto))
001514|       ('A'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::('s'::[])))))))))
001515|       Heap.empty
001516|   in
001517|   (*[2551]*)let (l0, s') = object_alloc s o in
001518|   (*[2551]*)let a = { attributes_data_value = (Coq_value_prim (Coq_prim_number
001519|     (of_int (my_Z_of_nat (length args))))); attributes_data_writable = true;
001520|     attributes_data_enumerable = false; attributes_data_configurable = true }
001521|   in
001522|   (*[2551]*)if_bool
001523|     (object_define_own_prop s' l0
001524|       ('l'::('e'::('n'::('g'::('t'::('h'::[]))))))
001525|       (descriptor_of_attributes (Coq_attributes_data_of a)) false)
001526|     (fun s1 b ->
001527|     (*[2551]*)if_void (arguments_object_map runs0 s1 c l0 xs args l str) (fun s2 ->
001528|       (*[2551]*)if str
001529|       then (*[78]*)let a0 = { attributes_data_value = (Coq_value_object lf);
001530|              attributes_data_writable = true; attributes_data_enumerable =
001531|              false; attributes_data_configurable = true }
001532|            in
001533|            (*[78]*)if_bool
001534|              (object_define_own_prop s2 l0
001535|                ('c'::('a'::('l'::('l'::('e'::('e'::[]))))))
001536|                (descriptor_of_attributes (Coq_attributes_data_of a0)) false)
001537|              (fun s3 b' -> (*[78]*)Coq_result_out (Coq_out_ter (s3,
001538|              (res_ref (Coq_resvalue_value (Coq_value_object l0))))))
001539|       else (*[2473]*)let vthrower = Coq_value_object (Coq_object_loc_prealloc
001540|              Coq_prealloc_throw_type_error)
001541|            in
001542|            (*[2473]*)let a0 = { attributes_accessor_get = vthrower;
001543|              attributes_accessor_set = vthrower;
001544|              attributes_accessor_enumerable = false;
001545|              attributes_accessor_configurable = false }
001546|            in
001547|            (*[2473]*)if_bool
001548|              (object_define_own_prop s2 l0
001549|                ('c'::('a'::('l'::('l'::('e'::('r'::[]))))))
001550|                (descriptor_of_attributes (Coq_attributes_accessor_of a0))
001551|                false) (fun s3 b' ->
001552|              (*[2473]*)if_bool
001553|                (object_define_own_prop s3 l0
001554|                  ('c'::('a'::('l'::('l'::('e'::('e'::[]))))))
001555|                  (descriptor_of_attributes (Coq_attributes_accessor_of a0))
001556|                  false) (fun s4 b'' -> (*[2473]*)Coq_result_out (Coq_out_ter (s4,
001557|                (res_ref (Coq_resvalue_value (Coq_value_object l0)))))))))
001558|  
001559| (** val binding_inst_arg_obj :
001560|     runs_type -> state -> execution_ctx -> object_loc -> prog -> char list
001561|     list -> value list -> env_loc -> result_void **)
001562|  
001563| let binding_inst_arg_obj runs0 s c lf p xs args l =
001564|   (*[2551]*)let arguments =
001565|     'a'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::('s'::[]))))))))
001566|   in
001567|   (*[2551]*)let str = prog_intro_strictness p in
001568|   (*[2551]*)if_object (create_arguments_object runs0 s c lf xs args l str)
001569|     (fun s1 largs ->
001570|     (*[2551]*)if str
001571|     then (*[78]*)if_void (env_record_create_immutable_binding s1 l arguments)
001572|            (fun s2 ->
001573|            (*[78]*)env_record_initialize_immutable_binding s2 l arguments
001574|              (Coq_value_object largs))
001575|     else (*[2473]*)env_record_create_set_mutable_binding runs0 s1 c l arguments None
001576|            (Coq_value_object largs) false)
001577|  
001578| (** val execution_ctx_binding_inst :
001579|     runs_type -> state -> execution_ctx -> codetype -> object_loc option ->
001580|     prog -> value list -> result_void **)
001581|  
001582| let execution_ctx_binding_inst runs0 s c ct funco p args =
001583|   (*[10465]*)destr_list c.execution_ctx_variable_env (fun x ->
001584|     (*[0]*)stuck_heap s
001585|       ('E'::('m'::('p'::('t'::('y'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('v'::('a'::('r'::('i'::('a'::('b'::('l'::('e'::('_'::('e'::('n'::('v'::(']'::(' '::('i'::('n'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001586|     (fun l x ->
001587|     (*[10465]*)let str = prog_intro_strictness p in
001588|     (*[10465]*)let follow = fun s' names ->
001589|       (*[10465]*)let bconfig = codetype_comparable ct Coq_codetype_eval in
001590|       (*[10465]*)let fds = prog_funcdecl p in
001591|       (*[10465]*)if_void (binding_inst_function_decls runs0 s' c l fds str bconfig)
001592|         (fun s1 ->
001593|         (*[10465]*)if_some
001594|           (env_record_has_binding s1 l
001595|             ('a'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::('s'::[]))))))))))
001596|           (fun bdefined ->
001597|           (*[10465]*)let follow2 = fun s'0 ->
001598|             (*[10465]*)let vds = prog_vardecl p in
001599|             (*[10465]*)binding_inst_var_decls runs0 s'0 c l vds str
001600|               (prog_intro_strictness p)
001601|           in
001602|           (match ct with
001603|            | Coq_codetype_func ->
001604|              (match funco with
001605|               | Some func ->
001606|                 (*[2555]*)if bdefined
001607|                 then (*[4]*)follow2 s1
001608|                 else (*[2551]*)if_void
001609|                        (binding_inst_arg_obj runs0 s1 c func p names args l)
001610|                        (fun s2 -> (*[2551]*)follow2 s2)
001611|               | None ->
001612|                 (*[0]*)if bdefined
001613|                 then (*[0]*)follow2 s1
001614|                 else (*[0]*)stuck_heap s1
001615|                        ('S'::('t'::('r'::('a'::('n'::('g'::('e'::(' '::('`'::('a'::('r'::('g'::('u'::('m'::('e'::('n'::('t'::('s'::('\''::(' '::('o'::('b'::('j'::('e'::('c'::('t'::(' '::('i'::('n'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001616|            | _ -> (*[7910]*)follow2 s1)))
001617|     in
001618|     (match ct with
001619|      | Coq_codetype_func ->
001620|        (match funco with
001621|         | Some func ->
001622|           (*[2555]*)if_some (run_object_method object_formal_parameters_ s func)
001623|             (fun names ->
001624|             (*[2555]*)if_void (binding_inst_formal_params runs0 s c l args names str)
001625|               (fun s' -> (*[2555]*)follow s' names))
001626|         | None ->
001627|           (*[0]*)stuck_heap s
001628|             ('N'::('o'::('t'::(' '::('c'::('o'::('h'::('e'::('r'::('e'::('n'::('t'::(' '::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::('n'::('a'::('l'::(' '::('c'::('o'::('d'::('e'::(' '::('t'::('y'::('p'::('e'::(' '::('i'::('n'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001629|      | Coq_codetype_global ->
001630|        (match funco with
001631|         | Some o ->
001632|           (*[0]*)stuck_heap s
001633|             ('N'::('o'::('t'::(' '::('c'::('o'::('h'::('e'::('r'::('e'::('n'::('t'::(' '::('n'::('o'::('n'::('-'::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::('n'::('a'::('l'::(' '::('c'::('o'::('d'::('e'::(' '::('t'::('y'::('p'::('e'::(' '::('i'::('n'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001634|         | None -> (*[7767]*)follow s [])
001635|      | Coq_codetype_eval ->
001636|        (match funco with
001637|         | Some o ->
001638|           (*[0]*)stuck_heap s
001639|             ('N'::('o'::('t'::(' '::('c'::('o'::('h'::('e'::('r'::('e'::('n'::('t'::(' '::('n'::('o'::('n'::('-'::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::('n'::('a'::('l'::(' '::('c'::('o'::('d'::('e'::(' '::('t'::('y'::('p'::('e'::(' '::('i'::('n'::(' '::('['::('e'::('x'::('e'::('c'::('u'::('t'::('i'::('o'::('n'::('_'::('c'::('t'::('x'::('_'::('b'::('i'::('n'::('d'::('i'::('n'::('g'::('_'::('i'::('n'::('s'::('t'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001640|         | None -> (*[143]*)follow s []))) ()
001641|  
001642| (** val run_call_default :
001643|     runs_type -> state -> execution_ctx -> object_loc -> result **)
001644|  
001645| let run_call_default runs0 s c lf =
001646|   (*[2555]*)let follow = fun o ->
001647|     (*[2517]*)if_success_or_return o (fun s' -> (*[1701]*)Coq_result_out (Coq_out_ter (s',
001648|       (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef))))))
001649|       (fun x x0 -> (*[581]*)Coq_result_out (Coq_out_ter (x, (res_ref x0))))
001650|   in
001651|   (*[2555]*)let default = Coq_out_ter (s,
001652|     (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef))))
001653|   in
001654|   (match run_object_method object_code_ s lf with
001655|    | Some bd ->
001656|      (*[2555]*)follow
001657|        (if eq_nil_dec (prog_elements (funcbody_prog bd))
001658|         then (*[22]*)Coq_result_out default
001659|         else (*[2533]*)runs0.runs_type_prog s c (funcbody_prog bd))
001660|    | None -> (*[0]*)follow (Coq_result_out default))
001661|  
001662| (** val entering_func_code :
001663|     runs_type -> state -> execution_ctx -> object_loc -> value -> value list
001664|     -> result **)
001665|  
001666| let entering_func_code runs0 s c lf vthis args =
001667|   (*[2555]*)if_some (run_object_method object_code_ s lf) (fun bd ->
001668|     (*[2555]*)let str = funcbody_is_strict bd in
001669|     (*[2555]*)let follow = fun s' vthis' ->
001670|       (*[2555]*)if_some (run_object_method object_scope_ s' lf) (fun lex ->
001671|         (*[2555]*)let (lex', s1) = lexical_env_alloc_decl s' lex in
001672|         (*[2555]*)let c' = execution_ctx_intro_same lex' vthis' str in
001673|         (*[2555]*)if_void
001674|           (execution_ctx_binding_inst runs0 s1 c' Coq_codetype_func (Some lf)
001675|             (funcbody_prog bd) args) (fun s2 ->
001676|           (*[2555]*)run_call_default runs0 s2 c' lf))
001677|     in
001678|     (*[2555]*)if str
001679|     then (*[78]*)follow s vthis
001680|     else (match vthis with
001681|           | Coq_value_prim p ->
001682|             (match p with
001683|              | Coq_prim_undef ->
001684|                (*[2043]*)follow s (Coq_value_object (Coq_object_loc_prealloc
001685|                  Coq_prealloc_global))
001686|              | Coq_prim_null ->
001687|                (*[0]*)follow s (Coq_value_object (Coq_object_loc_prealloc
001688|                  Coq_prealloc_global))
001689|              | _ -> (*[0]*)if_value (to_object s vthis) follow)
001690|           | Coq_value_object lthis -> (*[434]*)follow s vthis))
001691|  
001692| (** val run_object_has_instance_loop :
001693|     int -> state -> object_loc -> value -> result **)
001694|  
001695| let rec run_object_has_instance_loop max_step s lv vo =
001696|   (*[4]*)(fun fO fS n -> (*[4]*)if n=0 then (*[0]*)fO () else (*[4]*)fS (n-1))
001697|     (fun _ ->
001698|     (*[0]*)Coq_result_bottom)
001699|     (fun max_step' ->
001700|     match vo with
001701|     | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
001702|     | Coq_value_object lo ->
001703|       (match run_object_method object_proto_ s lv with
001704|        | Coq_value_prim p ->
001705|          (match p with
001706|           | Coq_prim_null ->
001707|             (*[1]*)Coq_result_out (Coq_out_ter (s,
001708|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001709|                 false))))))
001710|           | _ ->
001711|             (*[0]*)stuck_heap s
001712|               ('P'::('r'::('i'::('m'::('i'::('t'::('i'::('v'::('e'::(' '::('f'::('o'::('u'::('n'::('d'::(' '::('i'::('n'::(' '::('t'::('h'::('e'::(' '::('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::(' '::('c'::('h'::('a'::('i'::('n'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('o'::('b'::('j'::('e'::('c'::('t'::('_'::('h'::('a'::('s'::('_'::('i'::('n'::('s'::('t'::('a'::('n'::('c'::('e'::('_'::('l'::('o'::('o'::('p'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
001713|        | Coq_value_object proto ->
001714|          (*[3]*)if object_loc_comparable proto lo
001715|          then (*[1]*)Coq_result_out (Coq_out_ter (s,
001716|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001717|                   true))))))
001718|          else (*[2]*)run_object_has_instance_loop max_step' s proto
001719|                 (Coq_value_object lo)))
001720|     max_step
001721|  
001722| (** val run_object_has_instance :
001723|     int -> runs_type -> builtin_has_instance -> state -> execution_ctx ->
001724|     object_loc -> value -> result **)
001725|  
001726| let run_object_has_instance max_step runs0 b s c l v =
001727|   match b with
001728|   | Coq_builtin_has_instance_function ->
001729|     (match v with
001730|      | Coq_value_prim w ->
001731|        (*[0]*)Coq_result_out (Coq_out_ter (s,
001732|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001733|            false))))))
001734|      | Coq_value_object lv ->
001735|        (*[2]*)if_value
001736|          (object_get runs0 s c (Coq_value_object l)
001737|            ('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::[]))))))))))
001738|          (fun s1 v0 -> (*[2]*)run_object_has_instance_loop max_step s1 lv v0))
001739|   | Coq_builtin_has_instance_after_bind -> (*[0]*)(assert false) __
001740|  
001741| (** val is_lazy_op : binary_op -> bool option **)
001742|  
001743| let is_lazy_op = function
001744| | Coq_binary_op_and -> (*[71]*)Some false
001745| | Coq_binary_op_or -> (*[66]*)Some true
001746| | _ -> (*[27006]*)None
001747|  
001748| (** val get_puremath_op : binary_op -> number -> number -> number **)
001749|  
001750| let get_puremath_op = function
001751| | Coq_binary_op_mult -> (*[113]*)mult
001752| | Coq_binary_op_div -> (*[105]*)div
001753| | Coq_binary_op_mod -> (*[99]*)fmod
001754| | Coq_binary_op_sub -> (*[148]*)sub
001755| | _ -> (*[0]*)(assert false) __
001756|  
001757| (** val get_inequality_op : binary_op -> bool * bool **)
001758|  
001759| let get_inequality_op = function
001760| | Coq_binary_op_lt -> ((*[154]*)false, false)
001761| | Coq_binary_op_gt -> ((*[91]*)true, false)
001762| | Coq_binary_op_le -> ((*[99]*)true, true)
001763| | Coq_binary_op_ge -> ((*[99]*)false, true)
001764| | _ -> (*[0]*)(assert false) __
001765|  
001766| (** val get_shift_op : binary_op -> bool * (int -> int -> int) **)
001767|  
001768| let get_shift_op = function
001769| | Coq_binary_op_left_shift -> ((*[3324]*)false, int32_left_shift)
001770| | Coq_binary_op_right_shift -> ((*[2273]*)false, int32_right_shift)
001771| | Coq_binary_op_unsigned_right_shift -> ((*[2357]*)true, uint32_right_shift)
001772| | _ -> (*[0]*)(assert false) __
001773|  
001774| (** val get_bitwise_op : binary_op -> int -> int -> int **)
001775|  
001776| let get_bitwise_op = function
001777| | Coq_binary_op_bitwise_and -> (*[78]*)int32_bitwise_and
001778| | Coq_binary_op_bitwise_or -> (*[77]*)int32_bitwise_or
001779| | Coq_binary_op_bitwise_xor -> (*[74]*)int32_bitwise_xor
001780| | _ -> (*[0]*)(assert false) __
001781|  
001782| (** val convert_twice :
001783|     (result -> (state -> 'a1 -> result) -> result) -> (state -> value ->
001784|     result) -> state -> value -> value -> (state -> 'a1 -> 'a1 -> result) ->
001785|     result **)
001786|  
001787| let convert_twice ifv kC s v1 v2 k =
001788|   (*[10454]*)ifv (kC s v1) (fun s1 vc1 -> (*[10445]*)ifv (kC s1 v2) (fun s2 vc2 -> (*[10416]*)k s2 vc1 vc2))
001789|  
001790| (** val run_equal_partial :
001791|     int -> (state -> value -> result) -> (state -> value -> result) -> state
001792|     -> value -> value -> result **)
001793|  
001794| let rec run_equal_partial max_depth conv_number conv_primitive s v1 v2 =
001795|   (*[250]*)let k = fun t1 t2 ->
001796|     (*[121]*)let dc_conv = fun v3 f v4 ->
001797|       (*[97]*)if_value (f s v4) (fun s0 v2' ->
001798|         (*[89]*)(fun fO fS n -> (*[89]*)if n=0 then (*[0]*)fO () else (*[89]*)fS (n-1))
001799|           (fun _ ->
001800|           (*[0]*)Coq_result_bottom)
001801|           (fun max_depth' ->
001802|           (*[89]*)run_equal_partial max_depth' conv_number conv_primitive s0 v3 v2')
001803|           max_depth)
001804|     in
001805|     (*[121]*)let so = fun b -> (*[24]*)Coq_out_ter (s,
001806|       (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool b)))))
001807|     in
001808|     (*[121]*)if and_decidable
001809|          (or_decidable (type_comparable t1 Coq_type_null)
001810|            (type_comparable t1 Coq_type_undef))
001811|          (or_decidable (type_comparable t2 Coq_type_null)
001812|            (type_comparable t2 Coq_type_undef))
001813|     then (*[4]*)Coq_result_out (so true)
001814|     else (*[117]*)if and_decidable (type_comparable t1 Coq_type_number)
001815|               (type_comparable t2 Coq_type_string)
001816|          then (*[18]*)dc_conv v1 conv_number v2
001817|          else (*[99]*)if and_decidable (type_comparable t1 Coq_type_string)
001818|                    (type_comparable t2 Coq_type_number)
001819|               then (*[19]*)dc_conv v2 conv_number v1
001820|               else (*[80]*)if type_comparable t1 Coq_type_bool
001821|                    then (*[10]*)dc_conv v2 conv_number v1
001822|                    else (*[70]*)if type_comparable t2 Coq_type_bool
001823|                         then (*[14]*)dc_conv v1 conv_number v2
001824|                         else (*[56]*)if and_decidable
001825|                                   (or_decidable
001826|                                     (type_comparable t1 Coq_type_string)
001827|                                     (type_comparable t1 Coq_type_number))
001828|                                   (type_comparable t2 Coq_type_object)
001829|                              then (*[14]*)dc_conv v1 conv_primitive v2
001830|                              else (*[42]*)if and_decidable
001831|                                        (type_comparable t1 Coq_type_object)
001832|                                        (or_decidable
001833|                                          (type_comparable t2 Coq_type_string)
001834|                                          (type_comparable t2 Coq_type_number))
001835|                                   then (*[22]*)dc_conv v2 conv_primitive v1
001836|                                   else (*[20]*)Coq_result_out (so false)
001837|   in
001838|   (*[250]*)let t1 = type_of v1 in
001839|   (*[250]*)let t2 = type_of v2 in
001840|   (*[250]*)if type_comparable t1 t2
001841|   then (*[129]*)Coq_result_out (Coq_out_ter (s,
001842|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001843|            (equality_test_for_same_type t1 v1 v2)))))))
001844|   else (*[121]*)k t1 t2
001845|  
001846| (** val run_equal :
001847|     (state -> value -> result) -> (state -> value -> result) -> state ->
001848|     value -> value -> result **)
001849|  
001850| let run_equal =
001851|   (*[11745]*)run_equal_partial (Pervasives.succ (Pervasives.succ (Pervasives.succ
001852|     (Pervasives.succ 0))))
001853|  
001854| (** val run_binary_op :
001855|     int -> runs_type -> state -> execution_ctx -> binary_op -> value -> value
001856|     -> result **)
001857|  
001858| let run_binary_op max_step runs0 s c op v1 v2 =
001859|   (*[25133]*)let conv_primitive = fun s0 v -> (*[10477]*)to_primitive runs0 s0 c v None in
001860|   (*[25133]*)let convert_twice_primitive = convert_twice if_primitive conv_primitive in
001861|   (*[25133]*)let conv_number = fun s0 v -> (*[1365]*)to_number runs0 s0 c v in
001862|   (*[25133]*)let convert_twice_number = convert_twice if_number conv_number in
001863|   (*[25133]*)let conv_string = fun s0 v -> (*[9154]*)to_string runs0 s0 c v in
001864|   (*[25133]*)let convert_twice_string = convert_twice if_string conv_string in
001865|   (match op with
001866|    | Coq_binary_op_mult ->
001867|      (*[113]*)let mop = get_puremath_op op in
001868|      (*[113]*)convert_twice_number s v1 v2 (fun s1 n1 n2 -> (*[110]*)Coq_result_out
001869|        (Coq_out_ter (s1,
001870|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001871|          (mop n1 n2))))))))
001872|    | Coq_binary_op_div ->
001873|      (*[105]*)let mop = get_puremath_op op in
001874|      (*[105]*)convert_twice_number s v1 v2 (fun s1 n1 n2 -> (*[102]*)Coq_result_out
001875|        (Coq_out_ter (s1,
001876|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001877|          (mop n1 n2))))))))
001878|    | Coq_binary_op_mod ->
001879|      (*[99]*)let mop = get_puremath_op op in
001880|      (*[99]*)convert_twice_number s v1 v2 (fun s1 n1 n2 -> (*[96]*)Coq_result_out
001881|        (Coq_out_ter (s1,
001882|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001883|          (mop n1 n2))))))))
001884|    | Coq_binary_op_add ->
001885|      (*[4780]*)convert_twice_primitive s v1 v2 (fun s1 w1 w2 ->
001886|        (*[4766]*)if or_decidable
001887|             (type_comparable (type_of (Coq_value_prim w1)) Coq_type_string)
001888|             (type_comparable (type_of (Coq_value_prim w2)) Coq_type_string)
001889|        then (*[4577]*)convert_twice_string s1 (Coq_value_prim w1) (Coq_value_prim w2)
001890|               (fun s2 s3 s4 -> (*[4577]*)Coq_result_out (Coq_out_ter (s2,
001891|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
001892|                 (append s3 s4))))))))
001893|        else (*[189]*)convert_twice_number s1 (Coq_value_prim w1) (Coq_value_prim w2)
001894|               (fun s2 n1 n2 -> (*[189]*)Coq_result_out (Coq_out_ter (s2,
001895|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001896|                 (add n1 n2)))))))))
001897|    | Coq_binary_op_sub ->
001898|      (*[148]*)let mop = get_puremath_op op in
001899|      (*[148]*)convert_twice_number s v1 v2 (fun s1 n1 n2 -> (*[145]*)Coq_result_out
001900|        (Coq_out_ter (s1,
001901|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001902|          (mop n1 n2))))))))
001903|    | Coq_binary_op_left_shift ->
001904|      (*[3324]*)let (b_unsigned, f) = get_shift_op op in
001905|      (*[3324]*)if b_unsigned
001906|      then (*[0]*)to_uint32 runs0 s c v1 (fun s1 k1 ->
001907|             (*[0]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001908|               (*[0]*)let k2' = modulo_32 k2 in
001909|               (*[0]*)Coq_result_out (Coq_out_ter (s2,
001910|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001911|                 (of_int (f k1 k2'))))))))))
001912|      else (*[3324]*)to_int32 runs0 s c v1 (fun s1 k1 ->
001913|             (*[3323]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001914|               (*[3321]*)let k2' = modulo_32 k2 in
001915|               (*[3321]*)Coq_result_out (Coq_out_ter (s2,
001916|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001917|                 (of_int (f k1 k2'))))))))))
001918|    | Coq_binary_op_right_shift ->
001919|      (*[2273]*)let (b_unsigned, f) = get_shift_op op in
001920|      (*[2273]*)if b_unsigned
001921|      then (*[0]*)to_uint32 runs0 s c v1 (fun s1 k1 ->
001922|             (*[0]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001923|               (*[0]*)let k2' = modulo_32 k2 in
001924|               (*[0]*)Coq_result_out (Coq_out_ter (s2,
001925|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001926|                 (of_int (f k1 k2'))))))))))
001927|      else (*[2273]*)to_int32 runs0 s c v1 (fun s1 k1 ->
001928|             (*[2272]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001929|               (*[2270]*)let k2' = modulo_32 k2 in
001930|               (*[2270]*)Coq_result_out (Coq_out_ter (s2,
001931|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001932|                 (of_int (f k1 k2'))))))))))
001933|    | Coq_binary_op_unsigned_right_shift ->
001934|      (*[2357]*)let (b_unsigned, f) = get_shift_op op in
001935|      (*[2357]*)if b_unsigned
001936|      then (*[2357]*)to_uint32 runs0 s c v1 (fun s1 k1 ->
001937|             (*[2354]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001938|               (*[2352]*)let k2' = modulo_32 k2 in
001939|               (*[2352]*)Coq_result_out (Coq_out_ter (s2,
001940|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001941|                 (of_int (f k1 k2'))))))))))
001942|      else (*[0]*)to_int32 runs0 s c v1 (fun s1 k1 ->
001943|             (*[0]*)to_uint32 runs0 s1 c v2 (fun s2 k2 ->
001944|               (*[0]*)let k2' = modulo_32 k2 in
001945|               (*[0]*)Coq_result_out (Coq_out_ter (s2,
001946|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001947|                 (of_int (f k1 k2'))))))))))
001948|    | Coq_binary_op_instanceof ->
001949|      (match v2 with
001950|       | Coq_value_prim p -> (*[1]*)run_error s Coq_native_error_type
001951|       | Coq_value_object l ->
001952|         (*[320]*)morph_option (fun x -> (*[317]*)run_error s Coq_native_error_type)
001953|           (fun has_instance_id x ->
001954|           (*[2]*)run_object_has_instance max_step runs0 has_instance_id s c l v1)
001955|           (run_object_method object_has_instance_ s l) ())
001956|    | Coq_binary_op_in ->
001957|      (match v2 with
001958|       | Coq_value_prim p -> (*[1]*)run_error s Coq_native_error_type
001959|       | Coq_value_object l ->
001960|         (*[17]*)if_string (to_string runs0 s c v1) (fun s2 x ->
001961|           (*[17]*)if_some (object_has_prop s2 l x) (fun x0 -> (*[17]*)Coq_result_out
001962|             (Coq_out_ter (s2,
001963|             (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001964|               x0)))))))))
001965|    | Coq_binary_op_equal ->
001966|      (*[76]*)let finalPass = fun b ->
001967|        match op with
001968|        | Coq_binary_op_equal -> (*[72]*)b
001969|        | Coq_binary_op_disequal -> (*[0]*)negb b
001970|        | _ -> (*[0]*)(assert false) __
001971|      in
001972|      (*[76]*)if_bool (run_equal conv_number conv_primitive s v1 v2) (fun s0 b0 ->
001973|        (*[72]*)Coq_result_out (Coq_out_ter (s0,
001974|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001975|          (finalPass b0))))))))
001976|    | Coq_binary_op_disequal ->
001977|      (*[85]*)let finalPass = fun b ->
001978|        match op with
001979|        | Coq_binary_op_equal -> (*[0]*)b
001980|        | Coq_binary_op_disequal -> (*[81]*)negb b
001981|        | _ -> (*[0]*)(assert false) __
001982|      in
001983|      (*[85]*)if_bool (run_equal conv_number conv_primitive s v1 v2) (fun s0 b0 ->
001984|        (*[81]*)Coq_result_out (Coq_out_ter (s0,
001985|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001986|          (finalPass b0))))))))
001987|    | Coq_binary_op_strict_equal ->
001988|      (*[750]*)Coq_result_out (Coq_out_ter (s,
001989|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001990|          (strict_equality_test v1 v2)))))))
001991|    | Coq_binary_op_strict_disequal ->
001992|      (*[9987]*)Coq_result_out (Coq_out_ter (s,
001993|        (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
001994|          (negb (strict_equality_test v1 v2))))))))
001995|    | Coq_binary_op_bitwise_and ->
001996|      (*[81]*)to_int32 runs0 s c v1 (fun s1 k1 ->
001997|        (*[80]*)to_int32 runs0 s1 c v2 (fun s2 k2 -> (*[78]*)Coq_result_out (Coq_out_ter (s2,
001998|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
001999|            (of_int (get_bitwise_op op k1 k2))))))))))
002000|    | Coq_binary_op_bitwise_or ->
002001|      (*[80]*)to_int32 runs0 s c v1 (fun s1 k1 ->
002002|        (*[79]*)to_int32 runs0 s1 c v2 (fun s2 k2 -> (*[77]*)Coq_result_out (Coq_out_ter (s2,
002003|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
002004|            (of_int (get_bitwise_op op k1 k2))))))))))
002005|    | Coq_binary_op_bitwise_xor ->
002006|      (*[77]*)to_int32 runs0 s c v1 (fun s1 k1 ->
002007|        (*[76]*)to_int32 runs0 s1 c v2 (fun s2 k2 -> (*[74]*)Coq_result_out (Coq_out_ter (s2,
002008|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
002009|            (of_int (get_bitwise_op op k1 k2))))))))))
002010|    | Coq_binary_op_and ->
002011|      (*[0]*)stuck_heap s
002012|        ('U'::('n'::('d'::('e'::('a'::('l'::('t'::(' '::('l'::('a'::('z'::('y'::(' '::('o'::('p'::('e'::('r'::('a'::('t'::('o'::('r'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('b'::('i'::('n'::('a'::('r'::('y'::('_'::('o'::('p'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))
002013|    | Coq_binary_op_or ->
002014|      (*[0]*)stuck_heap s
002015|        ('U'::('n'::('d'::('e'::('a'::('l'::('t'::(' '::('l'::('a'::('z'::('y'::(' '::('o'::('p'::('e'::('r'::('a'::('t'::('o'::('r'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('b'::('i'::('n'::('a'::('r'::('y'::('_'::('o'::('p'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))
002016|    | Coq_binary_op_coma ->
002017|      (*[16]*)Coq_result_out (Coq_out_ter (s, (res_ref (Coq_resvalue_value v2))))
002018|    | _ ->
002019|      (*[443]*)let (b_swap, b_neg) = get_inequality_op op in
002020|      (*[443]*)convert_twice_primitive s v1 v2 (fun s1 w1 w2 ->
002021|        (*[431]*)if b_swap
002022|        then (*[184]*)let wr = inequality_test_primitive w2 w1 in
002023|             (*[184]*)Coq_result_out (Coq_out_ter (s1,
002024|             (if prim_comparable wr Coq_prim_undef
002025|              then (*[21]*)res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002026|                     false)))
002027|              else (*[163]*)if and_decidable (bool_comparable b_neg true)
002028|                        (prim_comparable wr (Coq_prim_bool true))
002029|                   then (*[14]*)res_ref (Coq_resvalue_value (Coq_value_prim
002030|                          (Coq_prim_bool false)))
002031|                   else (*[149]*)res_ref (Coq_resvalue_value (Coq_value_prim wr)))))
002032|        else (*[247]*)let wr = inequality_test_primitive w1 w2 in
002033|             (*[247]*)Coq_result_out (Coq_out_ter (s1,
002034|             (if prim_comparable wr Coq_prim_undef
002035|              then (*[21]*)res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002036|                     false)))
002037|              else (*[226]*)if and_decidable (bool_comparable b_neg true)
002038|                        (prim_comparable wr (Coq_prim_bool true))
002039|                   then (*[14]*)res_ref (Coq_resvalue_value (Coq_value_prim
002040|                          (Coq_prim_bool false)))
002041|                   else (*[212]*)res_ref (Coq_resvalue_value (Coq_value_prim wr)))))))
002042|  
002043| (** val run_prepost_op : unary_op -> (number -> number) * bool **)
002044|  
002045| let run_prepost_op = function
002046| | Coq_unary_op_post_incr -> ((*[80]*)add_one, false)
002047| | Coq_unary_op_post_decr -> ((*[26]*)sub_one, false)
002048| | Coq_unary_op_pre_incr -> ((*[43]*)add_one, true)
002049| | Coq_unary_op_pre_decr -> ((*[29]*)sub_one, true)
002050| | _ -> (*[0]*)(assert false) __
002051|  
002052| (** val run_typeof_value : state -> value -> char list **)
002053|  
002054| let run_typeof_value s = function
002055| | Coq_value_prim w -> (*[116]*)typeof_prim w
002056| | Coq_value_object l ->
002057|   (*[84]*)if is_callable_dec s (Coq_value_object l)
002058|   then (*[55]*)'f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::[])))))))
002059|   else (*[28]*)'o'::('b'::('j'::('e'::('c'::('t'::[])))))
002060|  
002061| (** val run_unary_op :
002062|     runs_type -> state -> execution_ctx -> unary_op -> expr -> result **)
002063|  
002064| let run_unary_op runs0 s c op e =
002065|   (*[7040]*)if prepost_unary_op_dec op
002066|   then (*[190]*)if_success (runs0.runs_type_expr s c e) (fun s1 rv1 ->
002067|          (*[190]*)if_success_value runs0 c (Coq_result_out (Coq_out_ter (s1,
002068|            (res_ref rv1)))) (fun s2 v2 ->
002069|            (*[186]*)if_number (to_number runs0 s2 c v2) (fun s3 n1 ->
002070|              (*[178]*)let (number_op, is_pre) = run_prepost_op op in
002071|              (*[178]*)let n2 = number_op n1 in
002072|              (*[178]*)let v = Coq_prim_number (if is_pre then (*[72]*)n2 else (*[106]*)n1) in
002073|              (*[178]*)if_void
002074|                (ref_put_value runs0 s3 c rv1 (Coq_value_prim (Coq_prim_number
002075|                  n2))) (fun s4 -> (*[178]*)Coq_result_out (Coq_out_ter (s4,
002076|                (res_ref (Coq_resvalue_value (Coq_value_prim v)))))))))
002077|   else (match op with
002078|         | Coq_unary_op_delete ->
002079|           (*[192]*)if_success (runs0.runs_type_expr s c e) (fun s1 rv ->
002080|             match rv with
002081|             | Coq_resvalue_empty ->
002082|               (*[0]*)stuck_heap s1
002083|                 ('E'::('m'::('p'::('t'::('y'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('f'::('o'::('r'::(' '::('a'::(' '::('`'::('d'::('e'::('l'::('e'::('t'::('e'::('\''::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('u'::('n'::('a'::('r'::('y'::('_'::('o'::('p'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))
002084|             | Coq_resvalue_value v ->
002085|               (*[3]*)Coq_result_out (Coq_out_ter (s1,
002086|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002087|                   true))))))
002088|             | Coq_resvalue_ref r ->
002089|               (*[89]*)if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_undef
002090|               then (*[3]*)Coq_result_out (Coq_out_ter (s1,
002091|                      (res_ref (Coq_resvalue_value (Coq_value_prim
002092|                        (Coq_prim_bool true))))))
002093|               else (match r.ref_base with
002094|                     | Coq_ref_base_type_value v ->
002095|                       (*[37]*)if_object (to_object s1 v) (fun s2 l ->
002096|                         (*[37]*)object_delete s2 l r.ref_name r.ref_strict)
002097|                     | Coq_ref_base_type_env_loc l ->
002098|                       (*[49]*)env_record_delete_binding s1 l r.ref_name))
002099|         | Coq_unary_op_typeof ->
002100|           (*[266]*)if_success (runs0.runs_type_expr s c e) (fun s1 rv ->
002101|             match rv with
002102|             | Coq_resvalue_empty ->
002103|               (*[0]*)stuck_heap s1
002104|                 ('E'::('m'::('p'::('t'::('y'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('f'::('o'::('r'::(' '::('a'::(' '::('`'::('t'::('y'::('p'::('e'::('o'::('f'::('\''::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('u'::('n'::('a'::('r'::('y'::('_'::('o'::('p'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))
002105|             | Coq_resvalue_value v ->
002106|               (*[50]*)Coq_result_out (Coq_out_ter (s1,
002107|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
002108|                   (run_typeof_value s1 v)))))))
002109|             | Coq_resvalue_ref r ->
002110|               (*[178]*)if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_undef
002111|               then (*[24]*)Coq_result_out (Coq_out_ter (s1,
002112|                      (res_ref (Coq_resvalue_value (Coq_value_prim
002113|                        (Coq_prim_string
002114|                        ('u'::('n'::('d'::('e'::('f'::('i'::('n'::('e'::('d'::[])))))))))))))))
002115|               else (*[154]*)if_success_value runs0 c (Coq_result_out (Coq_out_ter (s1,
002116|                      (res_ref (Coq_resvalue_ref r))))) (fun s2 v ->
002117|                      (*[150]*)Coq_result_out (Coq_out_ter (s2,
002118|                      (res_ref (Coq_resvalue_value (Coq_value_prim
002119|                        (Coq_prim_string (run_typeof_value s2 v)))))))))
002120|         | _ ->
002121|           (*[6392]*)if_success_value runs0 c (runs0.runs_type_expr s c e) (fun s1 v ->
002122|             match op with
002123|             | Coq_unary_op_void ->
002124|               (*[51]*)Coq_result_out (Coq_out_ter (s1,
002125|                 (res_ref (Coq_resvalue_value (Coq_value_prim
002126|                   Coq_prim_undef)))))
002127|             | Coq_unary_op_add -> (*[106]*)to_number runs0 s1 c v
002128|             | Coq_unary_op_neg ->
002129|               (*[5236]*)if_number (to_number runs0 s1 c v) (fun s2 n -> (*[5234]*)Coq_result_out
002130|                 (Coq_out_ter (s2,
002131|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
002132|                   (JsNumber.neg n))))))))
002133|             | Coq_unary_op_bitwise_not ->
002134|               (*[82]*)to_int32 runs0 s1 c v (fun s2 k -> (*[78]*)Coq_result_out (Coq_out_ter
002135|                 (s2,
002136|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
002137|                   (of_int (int32_bitwise_not k)))))))))
002138|             | Coq_unary_op_not ->
002139|               (*[640]*)Coq_result_out (Coq_out_ter (s1,
002140|                 (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002141|                   (neg (convert_value_to_boolean v))))))))
002142|             | _ ->
002143|               (*[0]*)stuck_heap s1
002144|                 ('U'::('n'::('d'::('e'::('a'::('l'::('t'::(' '::('r'::('e'::('g'::('u'::('l'::('a'::('r'::(' '::('o'::('p'::('e'::('r'::('a'::('t'::('o'::('r'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('u'::('n'::('a'::('r'::('y'::('_'::('o'::('p'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))
002145|  
002146| (** val init_object :
002147|     runs_type -> state -> execution_ctx -> object_loc -> propdefs -> result **)
002148|  
002149| let rec init_object runs0 s c l pds =
002150|   (*[25720]*)let create_new_function_in = fun s0 args bd ->
002151|     (*[0]*)creating_function_object runs0 s0 c args bd c.execution_ctx_lexical_env
002152|       c.execution_ctx_strict
002153|   in
002154|   (match pds with
002155|    | [] ->
002156|      (*[8689]*)Coq_result_out (Coq_out_ter (s,
002157|        (res_ref (Coq_resvalue_value (Coq_value_object l)))))
002158|    | p :: pds' ->
002159|      (*[17031]*)let (pn, pb) = p in
002160|      (*[17031]*)let x = string_of_propname pn in
002161|      (*[17031]*)let follows = fun s1 a ->
002162|        (*[17027]*)if_success
002163|          (object_define_own_prop s1 l x (descriptor_of_attributes a) false)
002164|          (fun s2 rv -> (*[17027]*)init_object runs0 s2 c l pds')
002165|      in
002166|      (match pb with
002167|       | Coq_propbody_val e0 ->
002168|         (*[17031]*)if_success_value runs0 c (runs0.runs_type_expr s c e0) (fun s1 v0 ->
002169|           (*[17027]*)let a = { attributes_data_value = v0; attributes_data_writable =
002170|             true; attributes_data_enumerable = true;
002171|             attributes_data_configurable = true }
002172|           in
002173|           (*[17027]*)follows s1 (Coq_attributes_data_of a))
002174|       | Coq_propbody_get bd ->
002175|         (*[0]*)if_value (create_new_function_in s [] bd) (fun s1 v0 ->
002176|           (*[0]*)let a = { attributes_accessor_get = (Coq_value_prim
002177|             Coq_prim_undef); attributes_accessor_set = v0;
002178|             attributes_accessor_enumerable = true;
002179|             attributes_accessor_configurable = true }
002180|           in
002181|           (*[0]*)follows s1 (Coq_attributes_accessor_of a))
002182|       | Coq_propbody_set (args, bd) ->
002183|         (*[0]*)if_value (create_new_function_in s args bd) (fun s1 v0 ->
002184|           (*[0]*)let a = { attributes_accessor_get = v0; attributes_accessor_set =
002185|             (Coq_value_prim Coq_prim_undef); attributes_accessor_enumerable =
002186|             true; attributes_accessor_configurable = true }
002187|           in
002188|           (*[0]*)follows s1 (Coq_attributes_accessor_of a))))
002189|  
002190| (** val run_var_decl :
002191|     runs_type -> state -> execution_ctx -> (prop_name * expr option) list ->
002192|     result **)
002193|  
002194| let rec run_var_decl runs0 s c = function
002195| | [] -> (*[2769]*)Coq_result_out (Coq_out_ter (s, res_empty))
002196| | y :: xeos' ->
002197|   (*[3452]*)let (x, eo) = y in
002198|   (*[3452]*)if_success
002199|     (match eo with
002200|      | Some e ->
002201|        (*[3339]*)if_success_value runs0 c (runs0.runs_type_expr s c e) (fun s1 v ->
002202|          (*[2693]*)if_some (identifier_res s1 c x) (fun ir ->
002203|            (*[2693]*)if_void (ref_put_value runs0 s1 c (Coq_resvalue_ref ir) v)
002204|              (fun s2 -> (*[2693]*)Coq_result_out (Coq_out_ter (s2,
002205|              (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef))))))))
002206|      | None ->
002207|        (*[113]*)Coq_result_out (Coq_out_ter (s,
002208|          (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef))))))
002209|     (fun s1 rv -> (*[2806]*)run_var_decl runs0 s1 c xeos')
002210|  
002211| (** val run_list_expr :
002212|     runs_type -> state -> execution_ctx -> value list -> expr list -> (state
002213|     -> value list -> result) -> result **)
002214|  
002215| let rec run_list_expr runs0 s1 c vs es k =
002216|   match es with
002217|   | [] -> (*[3284]*)k s1 (rev vs)
002218|   | e :: es' ->
002219|     (*[2989]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e) (fun s2 v ->
002220|       (*[2783]*)run_list_expr runs0 s2 c (v :: vs) es' k)
002221|  
002222| (** val run_block :
002223|     runs_type -> state -> execution_ctx -> resvalue -> stat list -> result **)
002224|  
002225| let rec run_block runs0 s c rv = function
002226| | [] -> (*[4347]*)Coq_result_out (Coq_out_ter (s, (res_ref rv)))
002227| | t :: ts' ->
002228|   (*[5766]*)if_success_state rv (runs0.runs_type_stat s c t) (fun s1 rv1 ->
002229|     (*[4170]*)run_block runs0 s1 c rv1 ts')
002230|  
002231| (** val run_expr_binary_op :
002232|     (state -> execution_ctx -> binary_op -> value -> value -> result) ->
002233|     runs_type -> state -> execution_ctx -> binary_op -> expr -> expr ->
002234|     result **)
002235|  
002236| let run_expr_binary_op run_binary_op' runs0 s c op e1 e2 =
002237|   match is_lazy_op op with
002238|   | Some b_ret ->
002239|     (*[137]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002240|       (*[115]*)let b1 = convert_value_to_boolean v1 in
002241|       (*[115]*)if bool_comparable b1 b_ret
002242|       then (*[44]*)Coq_result_out (Coq_out_ter (s1,
002243|              (res_ref (Coq_resvalue_value v1))))
002244|       else (*[71]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e2)
002245|              (fun x x0 -> (*[39]*)Coq_result_out (Coq_out_ter (x,
002246|              (res_ref (Coq_resvalue_value x0))))))
002247|   | None ->
002248|     (*[27006]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002249|       (*[24920]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e2) (fun s2 v2 ->
002250|         (*[24709]*)run_binary_op' s2 c op v1 v2))
002251|  
002252| (** val run_expr_access :
002253|     runs_type -> state -> execution_ctx -> expr -> expr -> result **)
002254|  
002255| let run_expr_access runs0 s c e1 e2 =
002256|   (*[4085]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002257|     (*[2067]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e2) (fun s2 v2 ->
002258|       (*[2067]*)if or_decidable (value_comparable v1 (Coq_value_prim Coq_prim_undef))
002259|            (value_comparable v1 (Coq_value_prim Coq_prim_null))
002260|       then (*[62]*)run_error s2 Coq_native_error_ref
002261|       else (*[2005]*)if_string (to_string runs0 s2 c v2) (fun s3 x -> (*[2005]*)Coq_result_out
002262|              (Coq_out_ter (s3,
002263|              (res_ref (Coq_resvalue_ref
002264|                (ref_create_value v1 x c.execution_ctx_strict))))))))
002265|  
002266| (** val run_expr_assign :
002267|     (state -> execution_ctx -> binary_op -> value -> value -> result) ->
002268|     runs_type -> state -> execution_ctx -> binary_op option -> expr -> expr
002269|     -> result **)
002270|  
002271| let run_expr_assign run_binary_op' runs0 s c opo e1 e2 =
002272|   (*[11850]*)if_success (runs0.runs_type_expr s c e1) (fun s1 rv1 ->
002273|     (*[11818]*)let follow = fun s0 rv' ->
002274|       match rv' with
002275|       | Coq_resvalue_value v ->
002276|         (*[11171]*)if_void (ref_put_value runs0 s0 c rv1 v) (fun s' -> (*[11060]*)Coq_result_out
002277|           (Coq_out_ter (s', (res_ref (Coq_resvalue_value v)))))
002278|       | _ ->
002279|         (*[0]*)stuck_heap s0
002280|           ('N'::('o'::('n'::('-'::('v'::('a'::('l'::('u'::('e'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('e'::('x'::('p'::('r'::('_'::('a'::('s'::('s'::('i'::('g'::('n'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))
002281|     in
002282|     (match opo with
002283|      | Some op ->
002284|        (*[446]*)if_success_value runs0 c (Coq_result_out (Coq_out_ter (s1,
002285|          (res_ref rv1)))) (fun s2 v1 ->
002286|          (*[435]*)if_success_value runs0 c (runs0.runs_type_expr s2 c e2)
002287|            (fun s3 v2 -> (*[424]*)if_success (run_binary_op' s3 c op v1 v2) follow))
002288|      | None ->
002289|        (*[11372]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e2) (fun s0 rv' ->
002290|          (*[10747]*)follow s0 (Coq_resvalue_value rv'))))
002291|  
002292| (** val run_expr_function :
002293|     runs_type -> state -> execution_ctx -> prop_name option -> char list list
002294|     -> funcbody -> result **)
002295|  
002296| let run_expr_function runs0 s c fo args bd =
002297|   match fo with
002298|   | Some fn ->
002299|     (*[29]*)let (lex', s') = lexical_env_alloc_decl s c.execution_ctx_lexical_env in
002300|     (*[29]*)let follow = fun l ->
002301|       (*[29]*)if_void (env_record_create_immutable_binding s' l fn) (fun s1 ->
002302|         (*[29]*)if_object
002303|           (creating_function_object runs0 s1 c args bd lex'
002304|             (funcbody_is_strict bd)) (fun s2 l0 ->
002305|           (*[29]*)if_void
002306|             (env_record_initialize_immutable_binding s2 l fn
002307|               (Coq_value_object l0)) (fun s3 -> (*[29]*)Coq_result_out (Coq_out_ter
002308|             (s3, (res_ref (Coq_resvalue_value (Coq_value_object l0))))))))
002309|     in
002310|     (*[29]*)destr_list lex' (fun x ->
002311|       (*[0]*)stuck_heap s'
002312|         ('E'::('m'::('p'::('t'::('y'::(' '::('l'::('e'::('x'::('i'::('c'::('a'::('l'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('a'::('l'::('l'::('o'::('c'::('a'::('t'::('e'::('d'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('e'::('x'::('p'::('r'::('_'::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
002313|       (fun l x -> (*[29]*)follow l) ()
002314|   | None ->
002315|     (*[9232]*)let lex = c.execution_ctx_lexical_env in
002316|     (*[9232]*)creating_function_object runs0 s c args bd lex (funcbody_is_strict bd)
002317|  
002318| (** val entering_eval_code :
002319|     runs_type -> state -> execution_ctx -> bool -> funcbody -> (state ->
002320|     execution_ctx -> result) -> result **)
002321|  
002322| let entering_eval_code runs0 s c direct bd k =
002323|   (*[143]*)let c' = if direct then (*[0]*)c else (*[143]*)execution_ctx_initial false in
002324|   (*[143]*)let str = funcbody_is_strict bd in
002325|   (*[143]*)let (lex, s') =
002326|     if str
002327|     then (*[0]*)lexical_env_alloc_decl s c'.execution_ctx_lexical_env
002328|     else ((*[143]*)c'.execution_ctx_lexical_env, s)
002329|   in
002330|   (*[143]*)let c1 = if str then (*[0]*)execution_ctx_with_lex_same c' lex else (*[143]*)c' in
002331|   (*[143]*)let p = funcbody_prog bd in
002332|   (*[143]*)if_void
002333|     (execution_ctx_binding_inst runs0 s' c1 Coq_codetype_eval None p [])
002334|     (fun s1 -> (*[143]*)k s1 c')
002335|  
002336| (** val run_eval :
002337|     runs_type -> state -> execution_ctx -> bool -> value -> value list ->
002338|     result **)
002339|  
002340| let run_eval runs0 s c is_direct_call vthis vs =
002341|   match get_arg 0 vs with
002342|   | Coq_value_prim p ->
002343|     (match p with
002344|      | Coq_prim_string s0 ->
002345|        (match parse_pickable s0 with
002346|         | Some p0 ->
002347|           (*[143]*)entering_eval_code runs0 s c is_direct_call (Coq_funcbody_intro
002348|             (p0, s0)) (fun s1 c' ->
002349|             (*[143]*)if_ter (runs0.runs_type_prog s1 c' p0) (fun s2 r ->
002350|               match r.res_type with
002351|               | Coq_restype_normal ->
002352|                 (match r.res_value with
002353|                  | Coq_resvalue_empty ->
002354|                    (*[89]*)Coq_result_out (Coq_out_ter (s2,
002355|                      (res_ref (Coq_resvalue_value (Coq_value_prim
002356|                        Coq_prim_undef)))))
002357|                  | Coq_resvalue_value v ->
002358|                    (*[41]*)Coq_result_out (Coq_out_ter (s2,
002359|                      (res_ref (Coq_resvalue_value v))))
002360|                  | Coq_resvalue_ref r0 ->
002361|                    (*[0]*)stuck_heap s2
002362|                      ('R'::('e'::('f'::('e'::('r'::('e'::('n'::('c'::('e'::(' '::('f'::('o'::('u'::('n'::('d'::(' '::('i'::('n'::(' '::('t'::('h'::('e'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('o'::('f'::(' '::('a'::('n'::(' '::('`'::('e'::('v'::('a'::('l'::('\''::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('e'::('v'::('a'::('l'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
002363|               | Coq_restype_throw ->
002364|                 (*[10]*)Coq_result_out (Coq_out_ter (s2, (res_throw r.res_value)))
002365|               | _ ->
002366|                 (*[0]*)stuck_heap s2
002367|                   ('F'::('o'::('r'::('b'::('i'::('d'::('d'::('e'::('n'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::(' '::('t'::('y'::('p'::('e'::(' '::('r'::('e'::('t'::('u'::('r'::('n'::('e'::('d'::(' '::('b'::('y'::(' '::('a'::('n'::(' '::('`'::('e'::('v'::('a'::('l'::('\''::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('e'::('v'::('a'::('l'::(']'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
002368|         | None -> (*[0]*)run_error s Coq_native_error_syntax)
002369|      | x ->
002370|        (*[5]*)Coq_result_out (Coq_out_ter (s,
002371|          (res_ref (Coq_resvalue_value (Coq_value_prim x))))))
002372|   | Coq_value_object o ->
002373|     (*[1]*)Coq_result_out (Coq_out_ter (s,
002374|       (res_ref (Coq_resvalue_value (Coq_value_object o)))))
002375|  
002376| (** val is_syntactic_eval : expr -> bool **)
002377|  
002378| let is_syntactic_eval = function
002379| | Coq_expr_literal l ->
002380|   (match l with
002381|    | Coq_literal_string s ->
002382|      (match s with
002383|       | [] -> (*[0]*)false
002384|       | a::s0 ->
002385|         (* If this appears, you're using Ascii internals. Please don't *)
002386|  (*[1]*)(fun f c ->
002387|   (*[1]*)let n = Char.code c in
002388|   (*[1]*)let h i = (*[8]*)(n land (1 lsl i)) <> 0 in
002389|   (*[1]*)f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
002390|           (fun b b0 b1 b2 b3 b4 b5 b6 ->
002391|           (*[1]*)if b
002392|           then (*[1]*)if b0
002393|                then (*[0]*)false
002394|                else (*[1]*)if b1
002395|                     then (*[0]*)if b2
002396|                          then (*[0]*)false
002397|                          else (*[0]*)if b3
002398|                               then (*[0]*)false
002399|                               else (*[0]*)if b4
002400|                                    then (*[0]*)if b5
002401|                                         then (*[0]*)if b6
002402|                                              then (*[0]*)false
002403|                                              else (match s0 with
002404|                                                    | [] -> (*[0]*)false
002405|                                                    | a0::s1 ->
002406|                                                      (* If this appears, you're using Ascii internals. Please don't *)
002407|  (*[0]*)(fun f c ->
002408|   (*[0]*)let n = Char.code c in
002409|   (*[0]*)let h i = (*[0]*)(n land (1 lsl i)) <> 0 in
002410|   (*[0]*)f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
002411|                                                        (fun b7 b8 b9 b10 b11 b12 b13 b14 ->
002412|                                                        (*[0]*)if b7
002413|                                                        then (*[0]*)false
002414|                                                        else (*[0]*)if b8
002415|                                                             then (*[0]*)if b9
002416|                                                                  then 
002417|                                                                    (*[0]*)if b10
002418|                                                                    then (*[0]*)false
002419|                                                                    else 
002420|                                                                     (*[0]*)if b11
002421|                                                                     then 
002422|                                                                     (*[0]*)if b12
002423|                                                                     then 
002424|                                                                     (*[0]*)if b13
002425|                                                                     then 
002426|                                                                     (*[0]*)if b14
002427|                                                                     then 
002428|                                                                     (*[0]*)false
002429|                                                                     else 
002430|                                                                     (match s1 with
002431|                                                                     | [] ->
002432|                                                                     (*[0]*)false
002433|                                                                     | a1::s2 ->
002434|                                                                     (* If this appears, you're using Ascii internals. Please don't *)
002435|  (*[0]*)(fun f c ->
002436|   (*[0]*)let n = Char.code c in
002437|   (*[0]*)let h i = (*[0]*)(n land (1 lsl i)) <> 0 in
002438|   (*[0]*)f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
002439|                                                                     (fun b15 b16 b17 b18 b19 b20 b21 b22 ->
002440|                                                                     (*[0]*)if b15
002441|                                                                     then 
002442|                                                                     (*[0]*)if b16
002443|                                                                     then 
002444|                                                                     (*[0]*)false
002445|                                                                     else 
002446|                                                                     (*[0]*)if b17
002447|                                                                     then 
002448|                                                                     (*[0]*)false
002449|                                                                     else 
002450|                                                                     (*[0]*)if b18
002451|                                                                     then 
002452|                                                                     (*[0]*)false
002453|                                                                     else 
002454|                                                                     (*[0]*)if b19
002455|                                                                     then 
002456|                                                                     (*[0]*)false
002457|                                                                     else 
002458|                                                                     (*[0]*)if b20
002459|                                                                     then 
002460|                                                                     (*[0]*)if b21
002461|                                                                     then 
002462|                                                                     (*[0]*)if b22
002463|                                                                     then 
002464|                                                                     (*[0]*)false
002465|                                                                     else 
002466|                                                                     (match s2 with
002467|                                                                     | [] ->
002468|                                                                     (*[0]*)false
002469|                                                                     | a2::s3 ->
002470|                                                                     (* If this appears, you're using Ascii internals. Please don't *)
002471|  (*[0]*)(fun f c ->
002472|   (*[0]*)let n = Char.code c in
002473|   (*[0]*)let h i = (*[0]*)(n land (1 lsl i)) <> 0 in
002474|   (*[0]*)f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
002475|                                                                     (fun b23 b24 b25 b26 b27 b28 b29 b30 ->
002476|                                                                     (*[0]*)if b23
002477|                                                                     then 
002478|                                                                     (*[0]*)false
002479|                                                                     else 
002480|                                                                     (*[0]*)if b24
002481|                                                                     then 
002482|                                                                     (*[0]*)false
002483|                                                                     else 
002484|                                                                     (*[0]*)if b25
002485|                                                                     then 
002486|                                                                     (*[0]*)if b26
002487|                                                                     then 
002488|                                                                     (*[0]*)if b27
002489|                                                                     then 
002490|                                                                     (*[0]*)false
002491|                                                                     else 
002492|                                                                     (*[0]*)if b28
002493|                                                                     then 
002494|                                                                     (*[0]*)if b29
002495|                                                                     then 
002496|                                                                     (*[0]*)if b30
002497|                                                                     then 
002498|                                                                     (*[0]*)false
002499|                                                                     else 
002500|                                                                     (match s3 with
002501|                                                                     | [] ->
002502|                                                                     (*[0]*)true
002503|                                                                     | a3::s4 ->
002504|                                                                     (*[0]*)false)
002505|                                                                     else 
002506|                                                                     (*[0]*)false
002507|                                                                     else 
002508|                                                                     (*[0]*)false
002509|                                                                     else 
002510|                                                                     (*[0]*)false
002511|                                                                     else 
002512|                                                                     (*[0]*)false)
002513|                                                                     a2)
002514|                                                                     else 
002515|                                                                     (*[0]*)false
002516|                                                                     else 
002517|                                                                     (*[0]*)false
002518|                                                                     else 
002519|                                                                     (*[0]*)false)
002520|                                                                     a1)
002521|                                                                     else 
002522|                                                                     (*[0]*)false
002523|                                                                     else 
002524|                                                                     (*[0]*)false
002525|                                                                     else 
002526|                                                                     (*[0]*)false
002527|                                                                  else (*[0]*)false
002528|                                                             else (*[0]*)false)
002529|                                                        a0)
002530|                                         else (*[0]*)false
002531|                                    else (*[0]*)false
002532|                     else (*[1]*)false
002533|           else (*[0]*)false)
002534|           a)
002535|    | _ -> (*[3]*)false)
002536| | _ -> (*[7801]*)false
002537|  
002538| (** val run_expr_call :
002539|     runs_type -> state -> execution_ctx -> expr -> expr list -> result **)
002540|  
002541| let run_expr_call runs0 s c e1 e2s =
002542|   (*[7805]*)let is_eval_direct = is_syntactic_eval e1 in
002543|   (*[7805]*)if_success (runs0.runs_type_expr s c e1) (fun s1 rv ->
002544|     (*[7289]*)if_success_value runs0 c (Coq_result_out (Coq_out_ter (s1,
002545|       (res_ref rv)))) (fun s2 f ->
002546|       (*[3176]*)run_list_expr runs0 s2 c [] e2s (fun s3 vs ->
002547|         match f with
002548|         | Coq_value_prim p -> (*[153]*)run_error s3 Coq_native_error_type
002549|         | Coq_value_object l ->
002550|           (*[2817]*)if neg_decidable (is_callable_dec s3 (Coq_value_object l))
002551|           then (*[6]*)run_error s3 Coq_native_error_type
002552|           else (*[2810]*)let follow = fun vthis ->
002553|                  (*[2810]*)if object_loc_comparable l (Coq_object_loc_prealloc
002554|                       Coq_prealloc_global_eval)
002555|                  then (*[277]*)run_eval runs0 s3 c is_eval_direct vthis vs
002556|                  else (*[2533]*)runs0.runs_type_call_full s3 c l vthis vs
002557|                in
002558|                (match rv with
002559|                 | Coq_resvalue_empty ->
002560|                   (*[0]*)stuck_heap s3
002561|                     ('['::('r'::('u'::('n'::('_'::('e'::('x'::('p'::('r'::('_'::('c'::('a'::('l'::('l'::(']'::(' '::('u'::('n'::('a'::('b'::('l'::('e'::(' '::('t'::('o'::(' '::('c'::('a'::('l'::('l'::(' '::('a'::('n'::(' '::(' '::('e'::('m'::('p'::('t'::('y'::(' '::('r'::('e'::('s'::('u'::('l'::('t'::('.'::[]))))))))))))))))))))))))))))))))))))))))))))))))
002562|                 | Coq_resvalue_value v ->
002563|                   (*[162]*)follow (Coq_value_prim Coq_prim_undef)
002564|                 | Coq_resvalue_ref r ->
002565|                   (match r.ref_base with
002566|                    | Coq_ref_base_type_value v ->
002567|                      (*[116]*)if or_decidable
002568|                           (ref_kind_comparable (ref_kind_of r)
002569|                             Coq_ref_kind_primitive_base)
002570|                           (ref_kind_comparable (ref_kind_of r)
002571|                             Coq_ref_kind_object)
002572|                      then (*[116]*)follow v
002573|                      else (*[0]*)stuck_heap s3
002574|                             ('['::('r'::('u'::('n'::('_'::('e'::('x'::('p'::('r'::('_'::('c'::('a'::('l'::('l'::(']'::(' '::('u'::('n'::('a'::('b'::('l'::('e'::(' '::('t'::('o'::(' '::('c'::('a'::('l'::('l'::(' '::('a'::(' '::('n'::('o'::('n'::('-'::('p'::('r'::('o'::('p'::('e'::('r'::('t'::('y'::(' '::('f'::('u'::('n'::('c'::('t'::('i'::('o'::('n'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))))))))))))
002575|                    | Coq_ref_base_type_env_loc l0 ->
002576|                      (*[2532]*)follow (env_record_implicit_this_value s3 l0))))))
002577|  
002578| (** val run_expr_conditionnal :
002579|     runs_type -> state -> execution_ctx -> expr -> expr -> expr -> result **)
002580|  
002581| let run_expr_conditionnal runs0 s c e1 e2 e3 =
002582|   (*[20]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002583|     (*[19]*)let b = convert_value_to_boolean v1 in
002584|     (*[19]*)let e = if b then (*[10]*)e2 else (*[9]*)e3 in
002585|     (*[19]*)if_success_value runs0 c (runs0.runs_type_expr s1 c e) (fun x x0 ->
002586|       (*[17]*)Coq_result_out (Coq_out_ter (x, (res_ref (Coq_resvalue_value x0))))))
002587|  
002588| (** val run_expr_new :
002589|     runs_type -> state -> execution_ctx -> expr -> expr list -> result **)
002590|  
002591| let run_expr_new runs0 s c e1 e2s =
002592|   (*[1170]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v ->
002593|     (*[314]*)run_list_expr runs0 s1 c [] e2s (fun s2 args ->
002594|       match v with
002595|       | Coq_value_prim p -> (*[14]*)run_error s2 Coq_native_error_type
002596|       | Coq_value_object l ->
002597|         (match run_object_method object_construct_ s l with
002598|          | Some c0 -> (*[279]*)run_construct runs0 s2 c l args
002599|          | None -> (*[13]*)run_error s2 Coq_native_error_type)))
002600|  
002601| (** val run_stat_label :
002602|     runs_type -> state -> execution_ctx -> label -> stat -> result **)
002603|  
002604| let run_stat_label runs0 s c lab t =
002605|   (*[13]*)if_break (runs0.runs_type_stat s c t) (fun s1 r1 -> (*[1]*)Coq_result_out
002606|     (Coq_out_ter (s1, (res_ref r1.res_value))))
002607|  
002608| (** val run_stat_with :
002609|     runs_type -> state -> execution_ctx -> expr -> stat -> result **)
002610|  
002611| let run_stat_with runs0 s c e1 t2 =
002612|   (*[148]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002613|     (*[148]*)if_object (to_object s1 v1) (fun s2 l ->
002614|       (*[129]*)let lex = c.execution_ctx_lexical_env in
002615|       (*[129]*)let (lex', s3) = lexical_env_alloc_object s2 lex l provide_this_true in
002616|       (*[129]*)let c' = execution_ctx_with_lex_this c lex' (Coq_value_object l) in
002617|       (*[129]*)runs0.runs_type_stat s3 c' t2))
002618|  
002619| (** val run_stat_if :
002620|     runs_type -> state -> execution_ctx -> expr -> stat -> stat option ->
002621|     result **)
002622|  
002623| let run_stat_if runs0 s c e1 t2 to0 =
002624|   (*[12610]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002625|     (*[10866]*)if convert_value_to_boolean v1
002626|     then (*[1632]*)runs0.runs_type_stat s1 c t2
002627|     else (match to0 with
002628|           | Some t3 -> (*[135]*)runs0.runs_type_stat s1 c t3
002629|           | None ->
002630|             (*[9099]*)Coq_result_out (Coq_out_ter (s1, (res_ref Coq_resvalue_empty)))))
002631|  
002632| (** val run_stat_while :
002633|     int -> runs_type -> resvalue -> state -> execution_ctx -> label_set ->
002634|     expr -> stat -> result **)
002635|  
002636| let rec run_stat_while max_step runs0 rv s c ls e1 t2 =
002637|   (*[77]*)(fun fO fS n -> (*[77]*)if n=0 then (*[0]*)fO () else (*[77]*)fS (n-1))
002638|     (fun _ ->
002639|     (*[0]*)Coq_result_bottom)
002640|     (fun max_step' ->
002641|     (*[77]*)let run_stat_while' = run_stat_while max_step' runs0 in
002642|     (*[77]*)if_success_value runs0 c (runs0.runs_type_expr s c e1) (fun s1 v1 ->
002643|       (*[75]*)if convert_value_to_boolean v1
002644|       then (*[59]*)if_ter (runs0.runs_type_stat s1 c t2) (fun s2 r2 ->
002645|              (*[59]*)let rvR = r2.res_value in
002646|              (*[59]*)let rv' =
002647|                if resvalue_comparable rvR Coq_resvalue_empty then (*[5]*)rv else (*[54]*)rvR
002648|              in
002649|              (*[59]*)if_normal_continue_or_break (Coq_result_out (Coq_out_ter (s2,
002650|                r2))) (fun r -> (*[41]*)res_label_in r ls) (fun s3 r3 ->
002651|                (*[40]*)run_stat_while' rv' s3 c ls e1 t2) (fun s3 r3 ->
002652|                (*[14]*)Coq_result_out (Coq_out_ter (s3, (res_ref rv')))))
002653|       else (*[16]*)Coq_result_out (Coq_out_ter (s1, (res_ref rv)))))
002654|     max_step
002655|  
002656| (** val run_stat_try :
002657|     runs_type -> state -> execution_ctx -> stat -> (prop_name * stat) option
002658|     -> stat option -> result **)
002659|  
002660| let run_stat_try runs0 s c t1 t2o t3o =
002661|   (*[2544]*)let finally = fun res0 ->
002662|     match t3o with
002663|     | Some t3 ->
002664|       (*[84]*)if_ter res0 (fun s1 r ->
002665|         (*[84]*)if_success (runs0.runs_type_stat s1 c t3) (fun s2 rv' ->
002666|           (*[54]*)Coq_result_out (Coq_out_ter (s2, r))))
002667|     | None -> (*[2363]*)res0
002668|   in
002669|   (*[2544]*)if_any_or_throw (runs0.runs_type_stat s c t1) finally (fun s1 v ->
002670|     match t2o with
002671|     | Some y ->
002672|       (*[890]*)let (x, t2) = y in
002673|       (*[890]*)let lex = c.execution_ctx_lexical_env in
002674|       (*[890]*)let (lex', s') = lexical_env_alloc_decl s1 lex in
002675|       (match lex' with
002676|        | [] ->
002677|          (*[0]*)stuck_heap s1
002678|            ('E'::('m'::('p'::('t'::('y'::(' '::('l'::('e'::('x'::('i'::('c'::('a'::('l'::(' '::('e'::('n'::('v'::('i'::('r'::('o'::('n'::('n'::('m'::('e'::('n'::('t'::(' '::('i'::('n'::(' '::('['::('r'::('u'::('n'::('_'::('s'::('t'::('a'::('t'::('_'::('t'::('r'::('y'::(']'::('.'::[])))))))))))))))))))))))))))))))))))))))))))))
002679|        | l :: oldlex ->
002680|          (*[890]*)if_void
002681|            (env_record_create_set_mutable_binding runs0 s' c l x None v
002682|              throw_irrelevant) (fun s2 ->
002683|            (*[890]*)let c' = execution_ctx_with_lex c lex' in
002684|            (*[890]*)finally (runs0.runs_type_stat s2 c' t2)))
002685|     | None ->
002686|       (*[21]*)finally (Coq_result_out (Coq_out_ter (s1,
002687|         (res_throw (Coq_resvalue_value v))))))
002688|  
002689| (** val run_stat_throw :
002690|     runs_type -> state -> execution_ctx -> expr -> result **)
002691|  
002692| let run_stat_throw runs0 s c e =
002693|   (*[296]*)if_success_value runs0 c (runs0.runs_type_expr s c e) (fun s1 v1 ->
002694|     (*[293]*)Coq_result_out (Coq_out_ter (s1, (res_throw (Coq_resvalue_value v1)))))
002695|  
002696| (** val run_stat_return :
002697|     runs_type -> state -> execution_ctx -> expr option -> result **)
002698|  
002699| let run_stat_return runs0 s c = function
002700| | Some e ->
002701|   (*[707]*)if_success_value runs0 c (runs0.runs_type_expr s c e) (fun s1 v1 ->
002702|     (*[578]*)Coq_result_out (Coq_out_ter (s1, (res_return (Coq_resvalue_value v1)))))
002703| | None ->
002704|   (*[7]*)Coq_result_out (Coq_out_ter (s,
002705|     (res_return (Coq_resvalue_value (Coq_value_prim Coq_prim_undef)))))
002706|  
002707| (** val run_expr : int -> state -> execution_ctx -> expr -> result **)
002708|  
002709| let rec run_expr max_step s c e =
002710|   (*[157299]*)(fun fO fS n -> (*[157299]*)if n=0 then (*[0]*)fO () else (*[157299]*)fS (n-1))
002711|     (fun _ ->
002712|     (*[0]*)Coq_result_bottom)
002713|     (fun max_step' ->
002714|     (*[157299]*)let run_expr' = run_expr max_step' in
002715|     (*[157299]*)let run_stat' = run_stat max_step' in
002716|     (*[157299]*)let run_prog' = run_prog max_step' in
002717|     (*[157299]*)let run_call' = run_call max_step' in
002718|     (*[157299]*)let run_call_full' = run_call_full max_step' in
002719|     (*[157299]*)let runs' = { runs_type_expr = run_expr'; runs_type_stat = run_stat';
002720|       runs_type_prog = run_prog'; runs_type_call = run_call';
002721|       runs_type_call_full = run_call_full' }
002722|     in
002723|     (*[157299]*)let run_binary_op' = run_binary_op max_step' runs' in
002724|     (match e with
002725|      | Coq_expr_this ->
002726|        (*[409]*)Coq_result_out (Coq_out_ter (s,
002727|          (res_ref (Coq_resvalue_value c.execution_ctx_this_binding))))
002728|      | Coq_expr_identifier x ->
002729|        (*[36999]*)if_some (identifier_res s c x) (fun x0 -> (*[36999]*)Coq_result_out (Coq_out_ter
002730|          (s, (res_ref (Coq_resvalue_ref x0)))))
002731|      | Coq_expr_literal i ->
002732|        (*[38824]*)Coq_result_out (Coq_out_ter (s,
002733|          (res_ref (Coq_resvalue_value (Coq_value_prim
002734|            (convert_literal_to_prim i))))))
002735|      | Coq_expr_object pds ->
002736|        (*[8693]*)if_object (run_construct_prealloc runs' Coq_prealloc_object s c [])
002737|          (fun s1 l -> (*[8693]*)init_object runs' s1 c l pds)
002738|      | Coq_expr_function (fo, args, bd) ->
002739|        (*[9261]*)run_expr_function runs' s c fo args bd
002740|      | Coq_expr_access (e1, e2) -> (*[4085]*)run_expr_access runs' s c e1 e2
002741|      | Coq_expr_member (e1, f) ->
002742|        (*[4000]*)runs'.runs_type_expr s c (Coq_expr_access (e1, (Coq_expr_literal
002743|          (Coq_literal_string f))))
002744|      | Coq_expr_new (e1, e2s) -> (*[1170]*)run_expr_new runs' s c e1 e2s
002745|      | Coq_expr_call (e1, e2s) -> (*[7805]*)run_expr_call runs' s c e1 e2s
002746|      | Coq_expr_unary_op (op, e0) -> (*[7040]*)run_unary_op runs' s c op e0
002747|      | Coq_expr_binary_op (e1, op, e2) ->
002748|        (*[27143]*)run_expr_binary_op run_binary_op' runs' s c op e1 e2
002749|      | Coq_expr_conditional (e1, e2, e3) ->
002750|        (*[20]*)run_expr_conditionnal runs' s c e1 e2 e3
002751|      | Coq_expr_assign (e1, opo, e2) ->
002752|        (*[11850]*)run_expr_assign run_binary_op' runs' s c opo e1 e2))
002753|     max_step
002754|  
002755| (** val run_stat : int -> state -> execution_ctx -> stat -> result **)
002756|  
002757| and run_stat max_step s c t =
002758|   (*[43921]*)(fun fO fS n -> (*[43921]*)if n=0 then (*[0]*)fO () else (*[43921]*)fS (n-1))
002759|     (fun _ ->
002760|     (*[0]*)Coq_result_bottom)
002761|     (fun max_step' ->
002762|     (*[43921]*)let run_expr' = run_expr max_step' in
002763|     (*[43921]*)let run_stat' = run_stat max_step' in
002764|     (*[43921]*)let run_prog' = run_prog max_step' in
002765|     (*[43921]*)let run_call' = run_call max_step' in
002766|     (*[43921]*)let run_call_full' = run_call_full max_step' in
002767|     (*[43921]*)let runs' = { runs_type_expr = run_expr'; runs_type_stat = run_stat';
002768|       runs_type_prog = run_prog'; runs_type_call = run_call';
002769|       runs_type_call_full = run_call_full' }
002770|     in
002771|     (match t with
002772|      | Coq_stat_expr e ->
002773|        (*[18105]*)if_success_value runs' c (run_expr' s c e) (fun x x0 -> (*[12990]*)Coq_result_out
002774|          (Coq_out_ter (x, (res_ref (Coq_resvalue_value x0)))))
002775|      | Coq_stat_label (lab, t0) ->
002776|        (*[13]*)run_stat_label runs' s c (Coq_label_string lab) t0
002777|      | Coq_stat_block ts -> (*[5943]*)run_block runs' s c Coq_resvalue_empty ts
002778|      | Coq_stat_var_decl xeos -> (*[3415]*)run_var_decl runs' s c xeos
002779|      | Coq_stat_if (e1, t2, to0) -> (*[12610]*)run_stat_if runs' s c e1 t2 to0
002780|      | Coq_stat_while (ls, e1, t2) ->
002781|        (*[37]*)run_stat_while max_step' runs' Coq_resvalue_empty s c ls e1 t2
002782|      | Coq_stat_with (e1, t2) -> (*[148]*)run_stat_with runs' s c e1 t2
002783|      | Coq_stat_throw e -> (*[296]*)run_stat_throw runs' s c e
002784|      | Coq_stat_return eo -> (*[714]*)run_stat_return runs' s c eo
002785|      | Coq_stat_break so -> (*[19]*)Coq_result_out (Coq_out_ter (s, (res_break so)))
002786|      | Coq_stat_continue so ->
002787|        (*[26]*)Coq_result_out (Coq_out_ter (s, (res_continue so)))
002788|      | Coq_stat_try (t1, t2o, t3o) -> (*[2544]*)run_stat_try runs' s c t1 t2o t3o
002789|      | Coq_stat_debugger -> (*[0]*)Coq_result_out (Coq_out_ter (s, res_empty))
002790|      | _ -> (*[51]*)(assert false) __))
002791|     max_step
002792|  
002793| (** val run_elements :
002794|     int -> state -> execution_ctx -> resvalue -> element list -> result **)
002795|  
002796| and run_elements max_step s c rv els =
002797|   (*[47221]*)(fun fO fS n -> (*[47221]*)if n=0 then (*[0]*)fO () else (*[47221]*)fS (n-1))
002798|     (fun _ ->
002799|     (*[0]*)Coq_result_bottom)
002800|     (fun max_step' ->
002801|     (*[47221]*)let run_stat' = run_stat max_step' in
002802|     (*[47221]*)let run_elements' = run_elements max_step' in
002803|     (match els with
002804|      | [] -> (*[2766]*)Coq_result_out (Coq_out_ter (s, (res_ref rv)))
002805|      | e :: els' ->
002806|        (match e with
002807|         | Coq_element_stat t ->
002808|           (*[32669]*)if_not_throw (run_stat' s c t) (fun s1 r1 ->
002809|             (*[25573]*)let r2 = res_overwrite_value_if_empty rv r1 in
002810|             (*[25573]*)if_success (Coq_result_out (Coq_out_ter (s1, r2))) (fun s2 rv2 ->
002811|               (*[24992]*)run_elements' s2 c rv2 els'))
002812|         | Coq_element_func_decl (name, args, bd) -> (*[11786]*)run_elements' s c rv els')))
002813|     max_step
002814|  
002815| (** val run_prog : int -> state -> execution_ctx -> prog -> result **)
002816|  
002817| and run_prog max_step s c p =
002818|   (*[10443]*)(fun fO fS n -> (*[10443]*)if n=0 then (*[0]*)fO () else (*[10443]*)fS (n-1))
002819|     (fun _ ->
002820|     (*[0]*)Coq_result_bottom)
002821|     (fun max_step' ->
002822|     (*[10443]*)let run_elements' = run_elements max_step' in
002823|     (*[10443]*)let Coq_prog_intro (str, els) = p in
002824|     (*[10443]*)run_elements' s c Coq_resvalue_empty els)
002825|     max_step
002826|  
002827| (** val run_call :
002828|     int -> state -> execution_ctx -> prealloc -> value list -> result **)
002829|  
002830| and run_call max_step s c b args =
002831|   (*[756]*)(fun fO fS n -> (*[756]*)if n=0 then (*[0]*)fO () else (*[756]*)fS (n-1))
002832|     (fun _ ->
002833|     (*[0]*)Coq_result_bottom)
002834|     (fun max_step' ->
002835|     (*[756]*)let run_expr' = run_expr max_step' in
002836|     (*[756]*)let run_stat' = run_stat max_step' in
002837|     (*[756]*)let run_prog' = run_prog max_step' in
002838|     (*[756]*)let run_call' = run_call max_step' in
002839|     (*[756]*)let run_call_full' = run_call_full max_step' in
002840|     (*[756]*)let runs' = { runs_type_expr = run_expr'; runs_type_stat = run_stat';
002841|       runs_type_prog = run_prog'; runs_type_call = run_call';
002842|       runs_type_call_full = run_call_full' }
002843|     in
002844|     (match b with
002845|      | Coq_prealloc_global_is_finite ->
002846|        (*[4]*)let v = get_arg 0 args in
002847|        (*[4]*)if_number (to_number runs' s c v) (fun s0 n -> (*[4]*)Coq_result_out
002848|          (Coq_out_ter (s0,
002849|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002850|            (neg
002851|              (or_decidable (number_comparable n nan)
002852|                (or_decidable (number_comparable n infinity)
002853|                  (number_comparable n neg_infinity)))))))))))
002854|      | Coq_prealloc_global_is_nan ->
002855|        (*[186]*)let v = get_arg 0 args in
002856|        (*[186]*)if_number (to_number runs' s c v) (fun s0 n -> (*[186]*)Coq_result_out
002857|          (Coq_out_ter (s0,
002858|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002859|            (number_comparable n nan))))))))
002860|      | Coq_prealloc_object_get_proto_of ->
002861|        (*[0]*)let v = get_arg 0 args in
002862|        (*[0]*)if neg_decidable (type_comparable (type_of v) Coq_type_object)
002863|        then (*[0]*)Coq_result_stuck
002864|        else (*[0]*)Coq_result_out (Coq_out_ter (s,
002865|               (res_ref (Coq_resvalue_ref
002866|                 (ref_create_value v
002867|                   ('p'::('r'::('o'::('t'::('o'::('t'::('y'::('p'::('e'::[])))))))))
002868|                   false)))))
002869|      | Coq_prealloc_object_seal ->
002870|        (match get_arg 0 args with
002871|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
002872|         | Coq_value_object l ->
002873|           (*[0]*)let xs = object_properties_keys_as_list_pickable s l in
002874|           (*[0]*)let rec object_seal s0 = function
002875|           | [] ->
002876|             (*[0]*)let s1 = run_object_heap_set_extensible false s0 l in
002877|             (*[0]*)Coq_result_out (Coq_out_ter (s1,
002878|             (res_ref (Coq_resvalue_value (Coq_value_object l)))))
002879|           | x :: xs' ->
002880|             (*[0]*)if_some (run_object_get_own_prop s0 l x) (fun d ->
002881|               match d with
002882|               | Coq_full_descriptor_undef -> (*[0]*)Coq_result_stuck
002883|               | Coq_full_descriptor_some a ->
002884|                 (*[0]*)let a' =
002885|                   if attributes_configurable a
002886|                   then (*[0]*)let desc = { descriptor_value = None;
002887|                          descriptor_writable = None; descriptor_get = None;
002888|                          descriptor_set = None; descriptor_enumerable = None;
002889|                          descriptor_configurable = (Some false) }
002890|                        in
002891|                        (*[0]*)attributes_update a desc
002892|                   else (*[0]*)a
002893|                 in
002894|                 (*[0]*)if_void
002895|                   (object_define_own_prop s0 l x
002896|                     (descriptor_of_attributes a') true) (fun s1 ->
002897|                   (*[0]*)object_seal s1 xs'))
002898|           in (*[0]*)object_seal s xs)
002899|      | Coq_prealloc_object_freeze ->
002900|        (*[0]*)let v = get_arg 0 args in
002901|        (match v with
002902|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
002903|         | Coq_value_object l ->
002904|           (*[0]*)let xs = object_properties_keys_as_list_pickable s l in
002905|           (*[0]*)let rec object_freeze s0 = function
002906|           | [] ->
002907|             (*[0]*)let s1 = run_object_heap_set_extensible false s0 l in
002908|             (*[0]*)Coq_result_out (Coq_out_ter (s1,
002909|             (res_ref (Coq_resvalue_value (Coq_value_object l)))))
002910|           | x :: xs' ->
002911|             (*[0]*)if_some (run_object_get_own_prop s l x) (fun d ->
002912|               match d with
002913|               | Coq_full_descriptor_undef -> (*[0]*)Coq_result_stuck
002914|               | Coq_full_descriptor_some a ->
002915|                 (*[0]*)let a' =
002916|                   if and_decidable (attributes_is_data_dec a)
002917|                        (istrue_dec (attributes_writable a))
002918|                   then (*[0]*)let desc = { descriptor_value = None;
002919|                          descriptor_writable = (Some false); descriptor_get =
002920|                          None; descriptor_set = None; descriptor_enumerable =
002921|                          None; descriptor_configurable = None }
002922|                        in
002923|                        (*[0]*)attributes_update a desc
002924|                   else (*[0]*)a
002925|                 in
002926|                 (*[0]*)let a'' =
002927|                   if attributes_configurable a'
002928|                   then (*[0]*)let desc = { descriptor_value = None;
002929|                          descriptor_writable = None; descriptor_get = None;
002930|                          descriptor_set = None; descriptor_enumerable = None;
002931|                          descriptor_configurable = (Some false) }
002932|                        in
002933|                        (*[0]*)attributes_update a' desc
002934|                   else (*[0]*)a'
002935|                 in
002936|                 (*[0]*)if_void
002937|                   (object_define_own_prop s0 l x
002938|                     (descriptor_of_attributes a'') true) (fun s1 ->
002939|                   (*[0]*)object_freeze s1 xs'))
002940|           in (*[0]*)object_freeze s xs)
002941|      | Coq_prealloc_object_prevent_extensions ->
002942|        (*[0]*)let v = get_arg 0 args in
002943|        (match v with
002944|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
002945|         | Coq_value_object l ->
002946|           (*[0]*)let o = object_binds_pickable s l in
002947|           (*[0]*)let o1 = object_with_extension o false in
002948|           (*[0]*)let s' = object_write s l o1 in
002949|           (*[0]*)Coq_result_out (Coq_out_ter (s',
002950|           (res_ref (Coq_resvalue_value (Coq_value_object l))))))
002951|      | Coq_prealloc_object_is_sealed ->
002952|        (*[0]*)let v = get_arg 0 args in
002953|        (match v with
002954|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
002955|         | Coq_value_object l ->
002956|           (*[0]*)let xs = object_properties_keys_as_list_pickable s l in
002957|           (*[0]*)let rec object_is_sealed = function
002958|           | [] ->
002959|             (*[0]*)Coq_result_out (Coq_out_ter (s,
002960|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002961|                 (neg (run_object_method object_extensible_ s l))))))))
002962|           | x :: xs' ->
002963|             (*[0]*)if_some (run_object_get_own_prop s l x) (fun d ->
002964|               match d with
002965|               | Coq_full_descriptor_undef -> (*[0]*)Coq_result_stuck
002966|               | Coq_full_descriptor_some a ->
002967|                 (*[0]*)if attributes_configurable a
002968|                 then (*[0]*)Coq_result_out (Coq_out_ter (s,
002969|                        (res_ref (Coq_resvalue_value (Coq_value_prim
002970|                          (Coq_prim_bool false))))))
002971|                 else (*[0]*)object_is_sealed xs')
002972|           in (*[0]*)object_is_sealed xs)
002973|      | Coq_prealloc_object_is_frozen ->
002974|        (*[0]*)let v = get_arg 0 args in
002975|        (match v with
002976|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
002977|         | Coq_value_object l ->
002978|           (*[0]*)let xs = object_properties_keys_as_list_pickable s l in
002979|           (*[0]*)let rec object_is_frozen = function
002980|           | [] ->
002981|             (*[0]*)Coq_result_out (Coq_out_ter (s,
002982|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
002983|                 (neg (run_object_method object_extensible_ s l))))))))
002984|           | x :: xs' ->
002985|             (*[0]*)if_some (run_object_get_own_prop s l x) (fun d ->
002986|               (*[0]*)let check_configurable = fun a ->
002987|                 (*[0]*)if attributes_configurable a
002988|                 then (*[0]*)Coq_result_out (Coq_out_ter (s,
002989|                        (res_ref (Coq_resvalue_value (Coq_value_prim
002990|                          (Coq_prim_bool false))))))
002991|                 else (*[0]*)object_is_frozen xs'
002992|               in
002993|               (match d with
002994|                | Coq_full_descriptor_undef -> (*[0]*)Coq_result_stuck
002995|                | Coq_full_descriptor_some a ->
002996|                  (match a with
002997|                   | Coq_attributes_data_of ad ->
002998|                     (*[0]*)if attributes_writable (Coq_attributes_data_of ad)
002999|                     then (*[0]*)Coq_result_out (Coq_out_ter (s,
003000|                            (res_ref (Coq_resvalue_value (Coq_value_prim
003001|                              (Coq_prim_bool false))))))
003002|                     else (*[0]*)check_configurable (Coq_attributes_data_of ad)
003003|                   | Coq_attributes_accessor_of aa ->
003004|                     (*[0]*)check_configurable (Coq_attributes_accessor_of aa))))
003005|           in (*[0]*)object_is_frozen xs)
003006|      | Coq_prealloc_object_is_extensible ->
003007|        (*[0]*)let v = get_arg 0 args in
003008|        (match v with
003009|         | Coq_value_prim p -> (*[0]*)run_error s Coq_native_error_type
003010|         | Coq_value_object l ->
003011|           (*[0]*)Coq_result_out (Coq_out_ter (s,
003012|             (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
003013|               (run_object_method object_extensible_ s l))))))))
003014|      | Coq_prealloc_object_proto_to_string ->
003015|        (*[203]*)let v = c.execution_ctx_this_binding in
003016|        (match v with
003017|         | Coq_value_prim p ->
003018|           (match p with
003019|            | Coq_prim_undef ->
003020|              (*[0]*)Coq_result_out (Coq_out_ter (s,
003021|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
003022|                  ('['::('o'::('b'::('j'::('e'::('c'::('t'::(' '::('U'::('n'::('d'::('e'::('f'::('i'::('n'::('e'::('d'::(']'::[]))))))))))))))))))))))))
003023|            | Coq_prim_null ->
003024|              (*[0]*)Coq_result_out (Coq_out_ter (s,
003025|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
003026|                  ('['::('o'::('b'::('j'::('e'::('c'::('t'::(' '::('N'::('u'::('l'::('l'::(']'::[])))))))))))))))))))
003027|            | _ ->
003028|              (*[0]*)if_object (to_object s v) (fun s1 l ->
003029|                (*[0]*)let s0 = run_object_method object_class_ s l in
003030|                (*[0]*)Coq_result_out (Coq_out_ter (s1,
003031|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
003032|                  (append
003033|                    ('['::('o'::('b'::('j'::('e'::('c'::('t'::(' '::[]))))))))
003034|                    (append s0 (']'::[])))))))))))
003035|         | Coq_value_object o ->
003036|           (*[203]*)if_object (to_object s v) (fun s1 l ->
003037|             (*[203]*)let s0 = run_object_method object_class_ s l in
003038|             (*[203]*)Coq_result_out (Coq_out_ter (s1,
003039|             (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
003040|               (append
003041|                 ('['::('o'::('b'::('j'::('e'::('c'::('t'::(' '::[]))))))))
003042|                 (append s0 (']'::[])))))))))))
003043|      | Coq_prealloc_object_proto_value_of ->
003044|        (*[208]*)to_object s c.execution_ctx_this_binding
003045|      | Coq_prealloc_object_proto_is_prototype_of ->
003046|        (*[31]*)let v = get_arg 0 args in
003047|        (match v with
003048|         | Coq_value_prim w ->
003049|           (*[0]*)Coq_result_out (Coq_out_ter (s,
003050|             (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
003051|               false))))))
003052|         | Coq_value_object l ->
003053|           (*[31]*)let vt = c.execution_ctx_this_binding in
003054|           (*[31]*)if_object (to_object s vt) (fun s1 lo ->
003055|             (*[31]*)run_object_proto_is_prototype_of s1 lo l))
003056|      | Coq_prealloc_object_proto_prop_is_enumerable ->
003057|        (*[0]*)let v = get_arg 0 args in
003058|        (*[0]*)if_string (to_string runs' s c v) (fun s1 x ->
003059|          (*[0]*)if_object (to_object s1 c.execution_ctx_this_binding) (fun s2 l ->
003060|            (*[0]*)if_some (run_object_get_own_prop s2 l x) (fun d ->
003061|              match d with
003062|              | Coq_full_descriptor_undef ->
003063|                (*[0]*)Coq_result_out (Coq_out_ter (s2,
003064|                  (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
003065|                    false))))))
003066|              | Coq_full_descriptor_some a ->
003067|                (*[0]*)Coq_result_out (Coq_out_ter (s2,
003068|                  (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_bool
003069|                    (attributes_enumerable a))))))))))
003070|      | Coq_prealloc_function_proto ->
003071|        (*[3]*)Coq_result_out (Coq_out_ter (s,
003072|          (res_ref (Coq_resvalue_value (Coq_value_prim Coq_prim_undef)))))
003073|      | Coq_prealloc_bool ->
003074|        (*[0]*)let v = get_arg 0 args in
003075|        (*[0]*)let b0 = convert_value_to_boolean v in
003076|        (*[0]*)let o1 =
003077|          object_new (Coq_value_object (Coq_object_loc_prealloc
003078|            Coq_prealloc_bool_proto))
003079|            ('B'::('o'::('o'::('l'::('e'::('a'::('n'::[])))))))
003080|        in
003081|        (*[0]*)let o =
003082|          object_with_primitive_value o1 (Coq_value_prim (Coq_prim_bool b0))
003083|        in
003084|        (*[0]*)let (l, s') = object_alloc s o in
003085|        (*[0]*)Coq_result_out (Coq_out_ter (s',
003086|        (res_ref (Coq_resvalue_value (Coq_value_object l)))))
003087|      | Coq_prealloc_bool_proto_to_string ->
003088|        (*[0]*)if_bool (bool_proto_value_of_call s c) (fun s0 b0 -> (*[0]*)Coq_result_out
003089|          (Coq_out_ter (s0,
003090|          (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_string
003091|            (convert_bool_to_string b0))))))))
003092|      | Coq_prealloc_bool_proto_value_of -> (*[0]*)bool_proto_value_of_call s c
003093|      | Coq_prealloc_number ->
003094|        (*[0]*)if eq_nil_dec args
003095|        then (*[0]*)Coq_result_out (Coq_out_ter (s,
003096|               (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
003097|                 zero))))))
003098|        else (*[0]*)let v = get_arg 0 args in (*[0]*)to_number runs' s c v
003099|      | Coq_prealloc_number_proto_value_of ->
003100|        (*[0]*)let v = c.execution_ctx_this_binding in
003101|        (match run_value_viewable_as_prim
003102|                 ('N'::('u'::('m'::('b'::('e'::('r'::[])))))) s v with
003103|         | Some p ->
003104|           (match p with
003105|            | Coq_prim_number n ->
003106|              (*[0]*)Coq_result_out (Coq_out_ter (s,
003107|                (res_ref (Coq_resvalue_value (Coq_value_prim (Coq_prim_number
003108|                  n))))))
003109|            | _ -> (*[0]*)run_error s Coq_native_error_type)
003110|         | None -> (*[0]*)run_error s Coq_native_error_type)
003111|      | _ -> (*[121]*)(assert false) __))
003112|     max_step
003113|  
003114| (** val run_call_full :
003115|     int -> state -> execution_ctx -> object_loc -> value -> value list ->
003116|     result **)
003117|  
003118| and run_call_full max_step s c l vthis args =
003119|   (*[3311]*)(fun fO fS n -> (*[3311]*)if n=0 then (*[0]*)fO () else (*[3311]*)fS (n-1))
003120|     (fun _ ->
003121|     (*[0]*)Coq_result_bottom)
003122|     (fun max_step' ->
003123|     (*[3311]*)let run_expr' = run_expr max_step' in
003124|     (*[3311]*)let run_stat' = run_stat max_step' in
003125|     (*[3311]*)let run_prog' = run_prog max_step' in
003126|     (*[3311]*)let run_call' = run_call max_step' in
003127|     (*[3311]*)let run_call_full' = run_call_full max_step' in
003128|     (*[3311]*)let runs' = { runs_type_expr = run_expr'; runs_type_stat = run_stat';
003129|       runs_type_prog = run_prog'; runs_type_call = run_call';
003130|       runs_type_call_full = run_call_full' }
003131|     in
003132|     (*[3311]*)if_some (run_object_method object_call_ s l) (fun c0 ->
003133|       match c0 with
003134|       | Coq_call_default -> (*[2555]*)entering_func_code runs' s c l vthis args
003135|       | Coq_call_after_bind -> (*[0]*)Coq_result_stuck
003136|       | Coq_call_prealloc b -> (*[756]*)run_call' s c b args))
003137|     max_step
003138|  
003139| (** val runs : int -> runs_type **)
003140|  
003141| let runs max_step =
003142|   (*[14928]*)let run_expr' = run_expr max_step in
003143|   (*[14928]*)let run_stat' = run_stat max_step in
003144|   (*[14928]*)let run_prog' = run_prog max_step in
003145|   (*[14928]*)let run_call' = run_call max_step in
003146|   (*[14928]*)let run_call_full' = run_call_full max_step in
003147|   (*[14928]*){ runs_type_expr = run_expr'; runs_type_stat = run_stat'; runs_type_prog =
003148|   run_prog'; runs_type_call = run_call'; runs_type_call_full =
003149|   run_call_full' }
003150|  
003151| (** val run_javascript : int -> prog -> result **)
003152|  
003153| let run_javascript max_step p =
003154|   (*[7767]*)let runs' = runs max_step in
003155|   (*[7767]*)let p' = add_infos_prog strictness_false p in
003156|   (*[7767]*)let c = execution_ctx_initial (prog_intro_strictness p) in
003157|   (*[7767]*)if_void
003158|     (execution_ctx_binding_inst runs' state_initial c Coq_codetype_global
003159|       None p []) (fun s' -> (*[7767]*)runs'.runs_type_prog s' c p')
003160|  

Legend:
   some code - line containing no point
   some code - line containing only visited points
   some code - line containing only unvisited points
   some code - line containing both visited and unvisited points