JsInterpreter.ml

open Datatypes
open JsCommon
open JsCommonAux
open JsInit
open JsInterpreterMonads
open JsPreliminary
open JsSyntax
open JsSyntaxAux
open LibList
open LibOption
open LibProd
open List0
open Shared

(*------------JS preliminary -----------*)

(** val convert_number_to_bool : number -> bool **)

let convert_number_to_bool n =
  if    (n === JsNumber.zero) 
     || (n === JsNumber.neg_zero)
     || (n === JsNumber.nan)
  then false
  else true

(** val convert_string_to_bool : string -> bool **)

let convert_string_to_bool s =
  if string_eq s "" then false else true
  (* Arthur hack string.empty *)

(** val convert_prim_to_boolean : prim -> bool **)

let convert_prim_to_boolean _foo_ = match _foo_ with
| Coq_prim_undef -> false
| Coq_prim_null -> false
| Coq_prim_bool b -> b
| Coq_prim_number n -> convert_number_to_bool n
| Coq_prim_string s -> convert_string_to_bool s

(** val convert_value_to_boolean : value -> bool **)

let convert_value_to_boolean _foo_ = match _foo_ with
| Coq_value_prim p -> convert_prim_to_boolean p
| Coq_value_object o -> true

(** val convert_prim_to_number : prim -> number **)

let convert_prim_to_number _foo_ = match _foo_ with
| Coq_prim_undef -> JsNumber.nan
| Coq_prim_null -> JsNumber.zero
| Coq_prim_bool b -> if b then JsNumber.one else JsNumber.zero
| Coq_prim_number n -> n
| Coq_prim_string s -> JsNumber.from_string s

(** val convert_number_to_integer : number -> number **)

let convert_number_to_integer n =
  if n === JsNumber.nan
  then JsNumber.zero
  else if   (n === JsNumber.zero)
         || (n === JsNumber.neg_zero)
         || (n === JsNumber.infinity)
         || (n === JsNumber.neg_infinity)
       then n
       else  (JsNumber.sign n) *. (JsNumber.floor (JsNumber.absolute n))

(** val convert_bool_to_string : bool -> string **)

let convert_bool_to_string _foo_ = match _foo_ with
| true -> "true"
| false -> "false"

(** val convert_prim_to_string : prim -> string **)

let convert_prim_to_string _foo_ = match _foo_ with
| Coq_prim_undef ->
  "undefined"
| Coq_prim_null -> "null"
| Coq_prim_bool b -> convert_bool_to_string b
| Coq_prim_number n -> JsNumber.to_string n
| Coq_prim_string s -> s

(** val equality_test_for_same_type : coq_type -> value -> value -> bool **)

let equality_test_for_same_type ty v1 v2 =
  match ty with
  | Coq_type_undef -> true
  | Coq_type_null -> true
  | Coq_type_bool -> value_compare v1 v2
  | Coq_type_number ->
    (match v1 with
     | Coq_value_prim p ->
       (match p with
        | Coq_prim_undef -> false
        | Coq_prim_null -> false
        | Coq_prim_bool b -> false
        | Coq_prim_number n1 ->
          (match v2 with
           | Coq_value_prim p0 ->
             (match p0 with
              | Coq_prim_undef -> false
              | Coq_prim_null -> false
              | Coq_prim_bool b -> false
              | Coq_prim_number n2 ->
                if n1 === JsNumber.nan
                then false
                else if n2 === JsNumber.nan
                     then false
                     else if   (n1 === JsNumber.zero)
                            && (n2 === JsNumber.neg_zero)
                          then true
                          else if   (n1 === JsNumber.neg_zero)
                                &&  (n2 === JsNumber.zero)
                               then true
                               else n1 === n2
              | Coq_prim_string s -> false)
           | Coq_value_object o -> false)
        | Coq_prim_string s -> false)
     | Coq_value_object o -> false)
  | Coq_type_string -> value_compare v1 v2
  | Coq_type_object -> value_compare v1 v2

(** val strict_equality_test : value -> value -> bool **)

let strict_equality_test v1 v2 =
  let ty1 = type_of v1 in
  let ty2 = type_of v2 in
  if type_compare ty1 ty2
  then equality_test_for_same_type ty1 v1 v2
  else false

(** val inequality_test_number : number -> number -> prim **)

let inequality_test_number n1 n2 =
  if (n1 === JsNumber.nan) || (n2 === JsNumber.nan)
  then Coq_prim_undef
  else if n1 === n2
       then Coq_prim_bool false
       else if   (n1 === JsNumber.zero)
              && (n2 === JsNumber.neg_zero)
            then Coq_prim_bool false
            else if (n1 === JsNumber.neg_zero)
                 && (n2 === JsNumber.zero)
                 then Coq_prim_bool false
                 else if n1 === JsNumber.infinity
                      then Coq_prim_bool false
                      else if n2 === JsNumber.infinity
                           then Coq_prim_bool true
                           else if n2 === JsNumber.neg_infinity
                                then Coq_prim_bool false
                                else if n1 === JsNumber.neg_infinity
                                     then Coq_prim_bool true
                                     else Coq_prim_bool (n1 < n2)

(** val inequality_test_string : string -> string -> bool **)

(* ARTHUR hack 
let rec inequality_test_string s1 s2 =
  match s1 with
  | [] ->
    (match s2 with
     | [] -> false
     | a::s -> true)
  | c1::s1_2 ->
    (match s2 with
     | [] -> false
     | c2::s2_2 ->
       if ascii_comparable c1 c2
       then inequality_test_string s1_2 s2_2
       else lt_int_decidable (int_of_char c1) (int_of_char c2))
*)
let inequality_test_string s1 s2 = (not (string_eq s1 s2))


(** val inequality_test_primitive : prim -> prim -> prim **)

let inequality_test_primitive w1 w2 =
  match w1 with
  | Coq_prim_undef ->
    inequality_test_number (convert_prim_to_number w1)
      (convert_prim_to_number w2)
  | Coq_prim_null ->
    inequality_test_number (convert_prim_to_number w1)
      (convert_prim_to_number w2)
  | Coq_prim_bool b ->
    inequality_test_number (convert_prim_to_number w1)
      (convert_prim_to_number w2)
  | Coq_prim_number n ->
    inequality_test_number (convert_prim_to_number w1)
      (convert_prim_to_number w2)
  | Coq_prim_string s1 ->
    (match w2 with
     | Coq_prim_undef ->
       inequality_test_number (convert_prim_to_number w1)
         (convert_prim_to_number w2)
     | Coq_prim_null ->
       inequality_test_number (convert_prim_to_number w1)
         (convert_prim_to_number w2)
     | Coq_prim_bool b ->
       inequality_test_number (convert_prim_to_number w1)
         (convert_prim_to_number w2)
     | Coq_prim_number n ->
       inequality_test_number (convert_prim_to_number w1)
         (convert_prim_to_number w2)
     | Coq_prim_string s2 -> Coq_prim_bool (inequality_test_string s1 s2))

(** val typeof_prim : prim -> string **)

let typeof_prim _foo_ = match _foo_ with
| Coq_prim_undef ->
  "undefined"
| Coq_prim_null -> "object"
| Coq_prim_bool b -> "boolean"
| Coq_prim_number n -> "number"
| Coq_prim_string s -> "string"

(** val string_of_propname : propname -> prop_name **)

let string_of_propname _foo_ = match _foo_ with
| Coq_propname_identifier s -> s
| Coq_propname_string s -> s
| Coq_propname_number n -> JsNumber.to_string n

(*---------------------------------*)

(** val build_error : state -> value -> value -> result **)

let build_error s vproto vmsg =
  let o = object_new vproto ("Error") in
  let (l, s_2) = object_alloc s o in
  if value_compare vmsg (Coq_value_prim Coq_prim_undef)
  then result_out (Coq_out_ter (s_2, (res_val (Coq_value_object l))))
  else (fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
         ("Need [to_string] (this function shall be put in [runs_type].)")

(** val run_error : state -> native_error -> 'a1 specres **)

let run_error s ne =
  let%object (s_2, l) = (build_error s (Coq_value_object (Coq_object_loc_prealloc
                                                            (Coq_prealloc_native_error_proto ne))) (Coq_value_prim Coq_prim_undef)) in
  Coq_result_some (Coq_specret_out (Coq_out_ter (s_2,
                                                 (res_throw (Coq_resvalue_value (Coq_value_object l))))))

(** val out_error_or_void :
    state -> strictness_flag -> native_error -> result **)

let out_error_or_void s str ne =
  if str then run_error s ne else result_out (out_void s)

(** val out_error_or_cst :
    state -> strictness_flag -> native_error -> value -> result **)

let out_error_or_cst s str ne v =
  if str then run_error s ne else result_out (Coq_out_ter (s, (res_val v)))

(** val run_object_method :
    (coq_object -> 'a1) -> state -> object_loc -> 'a1 option **)

let run_object_method proj s l =
  LibOption.map proj (object_binds_pickable_option s l)

(*---DEBUG
  let run_object_method proj s l =
   let opt = object_binds_pickable_option s l in
     begin match opt with
       | None -> Debug.run_object_method l
       | _ -> ()
     end;
     LibOption.map proj opt
*)


(** val run_object_heap_set_extensible :
    bool -> state -> object_loc -> state option **)

let run_object_heap_set_extensible b s l =
  LibOption.map (fun o -> object_write s l (object_set_extensible o b))
    (object_binds_pickable_option s l)

(* DEBUG
   let run_object_heap_set_extensible b s l =
   let opt = object_binds_pickable_option s l in
     begin match opt with
       | None -> Debug.run_object_heap_set_extensible l
       | _ -> ()
     end;
     LibOption.map (fun o -> object_write s l (object_set_extensible o b)) opt
*)

(** val object_has_prop :
    state -> execution_ctx -> object_loc -> prop_name -> result **)

let rec object_has_prop s c l x =
  let%some b = (run_object_method object_has_prop_ s l) in
  match b with Coq_builtin_has_prop_default ->
    let%run (s1, d) = (run_object_get_prop s c l x) in
    res_ter s1
      (res_val (Coq_value_prim (Coq_prim_bool
                                  (not
                                     (full_descriptor_compare d Coq_full_descriptor_undef)))))

(** val object_get_builtin :
    state -> execution_ctx -> builtin_get -> value -> object_loc
    -> prop_name -> result **)

and object_get_builtin s c b vthis l x =
  let def s0 l0 =
    let%run (s1, d) = (run_object_get_prop s0 c l0 x) in
    match d with
    | Coq_full_descriptor_undef ->
      res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
    | Coq_full_descriptor_some a ->
      (match a with
       | Coq_attributes_data_of ad ->
         res_ter s1 (res_val ad.attributes_data_value)
       | Coq_attributes_accessor_of aa ->
         (match aa.attributes_accessor_get with
          | Coq_value_prim p ->
            (match p with
             | Coq_prim_undef ->
               res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
             | Coq_prim_null -> Coq_result_impossible
             | Coq_prim_bool b0 -> Coq_result_impossible
             | Coq_prim_number n -> Coq_result_impossible
             | Coq_prim_string s2 -> Coq_result_impossible)
          | Coq_value_object lf -> run_call s1 c lf vthis [])) in
  let function0 s0 =
    let%value (s_2, v) = (def s0 l) in
    if spec_function_get_error_case_dec s_2 x v
    then run_error s_2 Coq_native_error_type
    else res_ter s_2 (res_val v) in
  match b with
  | Coq_builtin_get_default -> def s l
  | Coq_builtin_get_function -> function0 s
  | Coq_builtin_get_args_obj ->
    let%some lmapo = (run_object_method object_parameter_map_ s l) in
    let%some lmap = (lmapo) in
    let%run (s0, d) = (run_object_get_own_prop s c lmap x) in
    match d with
    | Coq_full_descriptor_undef -> function0 s0
    | Coq_full_descriptor_some a -> run_object_get s0 c lmap x

(** val run_object_get :
    state -> execution_ctx -> object_loc -> prop_name -> result **)

and run_object_get s c l x =
  let%some b = (run_object_method object_get_ s l) in
  object_get_builtin s c b (Coq_value_object l) l x

(** val run_object_get_prop :
    state -> execution_ctx -> object_loc -> prop_name ->
    full_descriptor specres **)

and run_object_get_prop s c l x =
  let%some b = (run_object_method object_get_prop_ s l) in
  match b with Coq_builtin_get_prop_default ->
    let%run (s1, d) = (run_object_get_own_prop s c l x) in
    if full_descriptor_compare d Coq_full_descriptor_undef
    then let%some proto = (run_object_method object_proto_ s1 l) in
      match proto with
      | Coq_value_prim p ->
        (match p with
         | Coq_prim_null -> res_spec s1 Coq_full_descriptor_undef
         | _ ->
           (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
             s1
             ("Found a non-null primitive value as a prototype in [run_object_get_prop]."))
      | Coq_value_object lproto ->
        run_object_get_prop s1 c lproto x
    else res_spec s1 d

(** val object_proto_is_prototype_of :
    state -> object_loc -> object_loc -> result **)

and object_proto_is_prototype_of s l0 l =
  let%some b = (run_object_method object_proto_ s l) in
  match b with
  | Coq_value_prim p ->
    (match p with
     | Coq_prim_null ->
       result_out (Coq_out_ter (s,
                                (res_val (Coq_value_prim (Coq_prim_bool false)))))
     | _ ->
       (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
         s
         ("[run_object_method] returned a primitive in [object_proto_is_prototype_of_body]."))
  | Coq_value_object l_2 ->
    if object_loc_compare l_2 l0
    then result_out (Coq_out_ter (s,
                                  (res_val (Coq_value_prim (Coq_prim_bool true)))))
    else object_proto_is_prototype_of s l0 l_2

(** val object_default_value :
    state -> execution_ctx -> object_loc -> preftype option ->
    result **)

and object_default_value s c l prefo =
  let%some b = (run_object_method object_default_value_ s l) in
  match b with Coq_builtin_default_value_default ->
    let gpref = unsome_default Coq_preftype_number prefo in
    let lpref = other_preftypes gpref in
    let sub0 s_2 x k =
      let%value (s1, vfo) = (run_object_get s_2 c l x) in
      let%some co = (run_callable s1 vfo) in
      match co with
      | Some b0 ->
        let%object (s2, lfunc) = (result_out (Coq_out_ter (s1, (res_val vfo)))) in
        let%value (s3, v) = (run_call s2 c lfunc (Coq_value_object l) []) in begin
          match v with
          | Coq_value_prim w ->
            result_out (Coq_out_ter (s3, (res_val (Coq_value_prim w))))
          | Coq_value_object l0 -> k s3
        end
      | None -> k s1 in
    let gmeth = (method_of_preftype gpref) in
    sub0 s gmeth (fun s_2 ->
        let lmeth = method_of_preftype lpref in
        sub0 s_2 lmeth (fun s_3 -> run_error s_3 Coq_native_error_type))

(** val to_primitive :
    state -> execution_ctx -> value -> preftype option -> result **)

and to_primitive s c v prefo =
  match v with
  | Coq_value_prim w ->
    result_out (Coq_out_ter (s, (res_val (Coq_value_prim w))))
  | Coq_value_object l ->
    let%prim (s0, r) = (object_default_value s c l prefo) in
    res_ter s0 (res_val (Coq_value_prim r))

(** val to_number :
    state -> execution_ctx -> value -> result **)

and to_number s c _foo_ = match _foo_ with
  | Coq_value_prim w ->
    result_out (Coq_out_ter (s, (res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w))))))
  | Coq_value_object l ->
    let%prim (s1, w) = (to_primitive s c (Coq_value_object l) (Some Coq_preftype_number)) in
    res_ter s1 (res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w))))

(** val to_integer :
    state -> execution_ctx -> value -> result **)

and to_integer s c v =
  let%number (s1, n) = to_number s c v in
  res_ter s1
    (res_val (Coq_value_prim (Coq_prim_number
                                (convert_number_to_integer n))))

(** val to_int32 :
    state -> execution_ctx -> value -> float specres **)

and to_int32 s c v =
  let%number (s_2, n) = to_number s c v in res_spec s_2 (JsNumber.to_int32 n)

(** val to_uint32 :
    state -> execution_ctx -> value -> float specres **)

and to_uint32 s c v =
  let%number (s_2, n) = to_number s c v in res_spec s_2 (JsNumber.to_uint32 n)

(** val to_string :
    state -> execution_ctx -> value -> result **)

and to_string s c _foo_ = match _foo_ with
  | Coq_value_prim w ->
    result_out (Coq_out_ter (s,
                             (res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w))))))
  | Coq_value_object l ->
    let%prim (s1, w) = (to_primitive s c (Coq_value_object l) (Some Coq_preftype_string)) in
    res_ter s1
      (res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w))))

(** val object_can_put :
    state -> execution_ctx -> object_loc -> prop_name -> result **)

and object_can_put s c l x =
  let%some b = (run_object_method object_can_put_ s l) in
  match b with Coq_builtin_can_put_default ->
    let%run (s1, d) = (run_object_get_own_prop s c l x) in begin
      match d with
      | Coq_full_descriptor_undef ->
        let%some vproto = (run_object_method object_proto_ s1 l) in begin
          match vproto with
          | Coq_value_prim p ->
            (match p with
             | Coq_prim_null ->
               let%some b0= (run_object_method object_extensible_ s1 l) in
               res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool b0)))
             | _ ->
               (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
                 s1
                 ("Non-null primitive get as a prototype value in [object_can_put]."))
          | Coq_value_object lproto ->
            let%run (s2, d_2) = (run_object_get_prop s1 c lproto x) in
            match d_2 with
            | Coq_full_descriptor_undef ->
              let%some b0= (run_object_method object_extensible_ s2 l) in
              res_ter s2 (res_val (Coq_value_prim (Coq_prim_bool b0)))
            | Coq_full_descriptor_some a ->
              (match a with
               | Coq_attributes_data_of ad ->
                 let%some ext = (run_object_method object_extensible_ s2 l) in
                 res_ter s2
                   (if ext
                    then res_val (Coq_value_prim (Coq_prim_bool
                                                    ad.attributes_data_writable))
                    else res_val (Coq_value_prim (Coq_prim_bool false)))
               | Coq_attributes_accessor_of aa ->
                 res_ter s2
                   (res_val (Coq_value_prim (Coq_prim_bool
                                               (not
                                                  (value_compare aa.attributes_accessor_set
                                                     (Coq_value_prim Coq_prim_undef)))))))
        end
      | Coq_full_descriptor_some a ->
        (match a with
         | Coq_attributes_data_of ad ->
           res_ter s1
             (res_val (Coq_value_prim (Coq_prim_bool
                                         ad.attributes_data_writable)))
         | Coq_attributes_accessor_of aa ->
           res_ter s1
             (res_val (Coq_value_prim (Coq_prim_bool
                                         (not
                                            (value_compare aa.attributes_accessor_set (Coq_value_prim
                                                                                            Coq_prim_undef)))))))
    end

(** val run_object_define_own_prop_array_loop :
    state -> execution_ctx -> object_loc -> float -> float ->
    descriptor -> bool -> bool -> (state -> prop_name -> descriptor ->
    strictness_flag -> __ specres) -> result **)

and run_object_define_own_prop_array_loop s c l newLen oldLen newLenDesc newWritable throwcont def =
  if newLen < oldLen
  then let oldLen_2 = (oldLen -. 1.) in
    let%string (s0, slen) = (to_string s c (Coq_value_prim (Coq_prim_number oldLen_2))) in
    let%bool (s1, deleteSucceeded) = (object_delete s0 c l slen false) in
    if not deleteSucceeded
    then let newLenDesc0 =
           (descriptor_with_value
              newLenDesc
              (Some (Coq_value_prim
                       (Coq_prim_number (oldLen_2 +. 1.))))) in
      let newLenDesc1 = (if not newWritable
                         then descriptor_with_writable newLenDesc0 (Some false)
                         else newLenDesc0) in
      let%bool (s2, x) = (def s1 ("length")
                            newLenDesc1 false) in
      out_error_or_cst s2 throwcont Coq_native_error_type
        (Coq_value_prim (Coq_prim_bool false))
    else run_object_define_own_prop_array_loop s1 c l
        newLen oldLen_2 newLenDesc newWritable throwcont def
  else if not newWritable
  then def s ("length")
      { descriptor_value = None; descriptor_writable = (Some false);
        descriptor_get = None; descriptor_set = None;
        descriptor_enumerable = None; descriptor_configurable = None }
      false
  else res_ter s (res_val (Coq_value_prim (Coq_prim_bool true)))

(** val object_define_own_prop :
    state -> execution_ctx -> object_loc -> prop_name ->
    descriptor -> strictness_flag -> result **)

and object_define_own_prop s c l x desc throwcont =
  let reject s0 throwcont0 =
    out_error_or_cst
      s0 throwcont0 Coq_native_error_type (Coq_value_prim
                                             (Coq_prim_bool false)) in
  let def s0 x0 desc0 throwcont0 =
    let%run (s1, d) = (run_object_get_own_prop s0 c l x0) in
    let%some ext = (run_object_method object_extensible_ s1 l) in
    match d with
    | Coq_full_descriptor_undef ->
      if ext
      then let a = (if (descriptor_is_generic_dec desc0) || (descriptor_is_data_dec desc0)
                    then Coq_attributes_data_of
                        (attributes_data_of_descriptor desc0)
                    else Coq_attributes_accessor_of
                        (attributes_accessor_of_descriptor desc0)) in
        let%some s2 = (object_heap_map_properties_pickable_option s1 l
                         (fun p -> HeapStr.write p x0 a)) in
        res_ter s2
          (res_val (Coq_value_prim (Coq_prim_bool true)))
      else reject s1 throwcont0
    | Coq_full_descriptor_some a ->
      let object_define_own_prop_write s2 a0 =
          let a_2 = attributes_update a0 desc0 in
          let%some s3 = (object_heap_map_properties_pickable_option s2 l (fun p -> HeapStr.write p x0 a_2)) in
          res_ter s3 (res_val (Coq_value_prim (Coq_prim_bool true))) in
      if descriptor_contains_dec (descriptor_of_attributes a) desc0
      then res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool true)))
      else if attributes_change_enumerable_on_non_configurable_dec a desc0
      then reject s1 throwcont0
      else if descriptor_is_generic_dec desc0
      then object_define_own_prop_write s1 a
      else if not (bool_eq (attributes_is_data_dec a) (descriptor_is_data_dec desc0))
      then if attributes_configurable a
        then let a_2 = (match a with
            | Coq_attributes_data_of ad ->
              Coq_attributes_accessor_of (attributes_accessor_of_attributes_data ad)
            | Coq_attributes_accessor_of aa ->
              Coq_attributes_data_of (attributes_data_of_attributes_accessor aa)) in
          let%some s2 = (object_heap_map_properties_pickable_option
                           s1 l (fun p -> HeapStr.write p x0 a_2)) in
          object_define_own_prop_write s2 a_2
        else reject s1 throwcont0
      else if (attributes_is_data_dec a) && (descriptor_is_data_dec desc0)
      then (match a with
          | Coq_attributes_data_of ad ->
            if attributes_change_data_on_non_configurable_dec ad desc0
            then reject s1 throwcont0
            else object_define_own_prop_write s1 a
          | Coq_attributes_accessor_of a0 ->
            (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
              s0
              ("data is not accessor in [defineOwnProperty]"))
      else if (not (attributes_is_data_dec a)) && (descriptor_is_accessor_dec desc0)
      then (match a with
          | Coq_attributes_data_of a0 ->
            (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
              s0
              ("accessor is not data in [defineOwnProperty]")
          | Coq_attributes_accessor_of aa ->
            if attributes_change_accessor_on_non_configurable_dec aa desc0
            then reject s1 throwcont0
            else object_define_own_prop_write s1 a)
      else (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
          s0
          ("cases are mutually exclusives in [defineOwnProperty]") in
  let%some b = (run_object_method object_define_own_prop_ s l) in
  match b with
  | Coq_builtin_define_own_prop_default -> def s x desc throwcont
  | Coq_builtin_define_own_prop_array ->
    let%run (s0, d) = (run_object_get_own_prop s c l ("length")) in begin
      match d with
      | Coq_full_descriptor_undef ->
        (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
          s0
          ("Array length property descriptor cannot be undefined.")
      | Coq_full_descriptor_some attr ->
        (match attr with
         | Coq_attributes_data_of a ->
           let  oldLen = (a.attributes_data_value) in begin
             match oldLen with
             | Coq_value_prim w ->
               let oldLen0 = (JsNumber.to_uint32 (convert_prim_to_number w)) in
               let descValueOpt = (desc.descriptor_value) in
               if string_eq x ("length")
               then (match descValueOpt with
                   | Some descValue ->
                     let%run (s1, newLen) = (to_uint32 s0 c descValue) in
                     let%number (s2, newLenN) = to_number s1 c descValue in
                     if not (newLen === newLenN)
                     then run_error s2 Coq_native_error_range
                     else let newLenDesc =
                            (descriptor_with_value desc (Some (Coq_value_prim (Coq_prim_number newLen)))) in
                       if le_int_decidable oldLen0 newLen
                       then def s2 ("length") newLenDesc throwcont
                       else if not a.attributes_data_writable
                       then reject s2 throwcont
                       else let newWritable = (match newLenDesc.descriptor_writable with
                           | Some b0 -> if b0 then true else false
                           | None -> true) in
                         let newLenDesc0 = (if not newWritable
                                            then descriptor_with_writable newLenDesc (Some true)
                                            else newLenDesc) in
                         let%bool (s3, succ) = (def s2 ("length") newLenDesc0 throwcont) in
                         if not succ
                         then res_ter s3 (res_val (Coq_value_prim (Coq_prim_bool false)))
                         else run_object_define_own_prop_array_loop s3 c l newLen oldLen0 newLenDesc0 newWritable throwcont def
                   | None -> def s0 ("length") desc throwcont)
               else let%run (s1, ilen) = (to_uint32 s0 c (Coq_value_prim (Coq_prim_string x))) in
                 let%string (s2, slen) = (to_string s1 c (Coq_value_prim (Coq_prim_number ilen))) in
                 if (string_eq x slen) && (not ( ilen = 4294967295.))
                 then let%run (s3, index) = (to_uint32 s2 c (Coq_value_prim (Coq_prim_string x))) in
                   if  (le_int_decidable oldLen0 index) && (not a.attributes_data_writable)
                   then reject s3 throwcont
                   else let%bool (s4, b0) = (def s3 x desc false) in
                     if not b0
                     then reject s4 throwcont
                     else if le_int_decidable oldLen0 index
                     then let a0 =
                            descriptor_with_value (descriptor_of_attributes (Coq_attributes_data_of a))
                              (Some (Coq_value_prim (Coq_prim_number (index +. 1.)))) in
                       def s4 ("length") a0 false
                     else res_ter s4 (res_val (Coq_value_prim (Coq_prim_bool true)))
                 else def s2 x desc throwcont
             | Coq_value_object l0 ->
               (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
                 s0
                 ("Spec asserts length of array is number.")
           end
         | Coq_attributes_accessor_of a ->
           (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
             s0
             ("Array length property descriptor cannot be accessor."))
    end
  | Coq_builtin_define_own_prop_args_obj ->
    let%some lmapo = (run_object_method object_parameter_map_ s l) in
    let%some lmap = (lmapo) in
    let%run (s0, d) = (run_object_get_own_prop s c lmap x) in
    let%bool (s1, b0) = (def s0 x desc false) in
    if b0
    then let follow s2 = res_ter s2 (res_val (Coq_value_prim (Coq_prim_bool true))) in
      match d with
      | Coq_full_descriptor_undef -> follow s1
      | Coq_full_descriptor_some a ->
        if descriptor_is_accessor_dec desc
        then let%bool (s2, x0) = (object_delete s1 c lmap x false) in follow s2
        else let follow0 s2 =
               if option_compare bool_eq desc.descriptor_writable (Some false)
               then let%bool (s3, x0) = (object_delete s2 c lmap x false) in
                 follow s3
               else follow s2 in
          match desc.descriptor_value with
          | Some v ->
            let%void s2 = (object_put s1 c lmap x v throwcont) in follow0 s2
          | None -> follow0 s1
    else reject s1 throwcont

(** val run_to_descriptor :
    state -> execution_ctx -> value -> descriptor specres **)

and run_to_descriptor s c _foo_ = match _foo_ with
  | Coq_value_prim p -> throw_result (run_error s Coq_native_error_type)
  | Coq_value_object l ->
    let sub0 s0 desc name conv k =
      let%bool (s1, has) = object_has_prop s0 c l name in
      if not has
      then k s1 desc
      else let%value (s2, v0) = run_object_get s1 c l name in
        let%run (s3, r) = conv s2 v0 desc in k s3 r
    in
    sub0 s descriptor_intro_empty ("enumerable")
      (fun s1 v1 desc ->
         let b = convert_value_to_boolean v1 in
         res_spec s1 (descriptor_with_enumerable desc (Some b))) (fun s1_2 desc ->
          sub0 s1_2 desc ("configurable")
            (fun s2 v2 desc0 ->
               let b = convert_value_to_boolean v2 in
               res_spec s2 (descriptor_with_configurable desc0 (Some b)))
            (fun s2_2 desc0 ->
               sub0 s2_2 desc0 ("value")
                 (fun s3 v3 desc1 ->
                    res_spec s3 (descriptor_with_value desc1 (Some v3)))
                 (fun s3_2 desc1 ->
                    sub0 s3_2 desc1
                      ("writable")
                      (fun s4 v4 desc2 ->
                         let b = convert_value_to_boolean v4 in
                         res_spec s4 (descriptor_with_writable desc2 (Some b)))
                      (fun s4_2 desc2 ->
                         sub0 s4_2 desc2 ("get") (fun s5 v5 desc3 ->
                             if (not (is_callable_dec s5 v5))
                             && (not (value_compare v5 (Coq_value_prim Coq_prim_undef)))
                             then throw_result (run_error s5 Coq_native_error_type)
                             else res_spec s5 (descriptor_with_get desc3 (Some v5)))
                           (fun s5_2 desc3 ->
                              sub0 s5_2 desc3 ("set") (fun s6 v6 desc4 ->
                                  if (not (is_callable_dec s6 v6))
                                  && (not (value_compare v6 (Coq_value_prim Coq_prim_undef)))
                                  then throw_result (run_error s6 Coq_native_error_type)
                                  else res_spec s6 (descriptor_with_set desc4 (Some v6)))
                                (fun s7 desc4 ->
                                   if ((not (option_compare value_compare desc4.descriptor_get None))
                                       ||
                                       (not (option_compare value_compare desc4.descriptor_set None)))
                                      &&
                                      ((not (option_compare value_compare desc4.descriptor_value None))
                                       ||
                                       (not (option_compare bool_eq desc4.descriptor_writable None)))
                                   then throw_result (run_error s7 Coq_native_error_type)
                                   else res_spec s7 desc4))))))

(** val prim_new_object : state -> prim -> result **)

and prim_new_object s _foo_ = match _foo_ with
  | Coq_prim_bool b ->
    result_out
      (let o1 = (object_new (Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_bool_proto)) ("Boolean")) in
       let o = (object_with_primitive_value o1 (Coq_value_prim (Coq_prim_bool b))) in
       let (l, s1) = object_alloc s o in
       Coq_out_ter (s1, (res_val (Coq_value_object l))))
  | Coq_prim_number n ->
    result_out
      (let o1 = (object_new (Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_number_proto)) ("Number")) in
       let o = (object_with_primitive_value o1 (Coq_value_prim (Coq_prim_number n))) in
       let (l, s1) = object_alloc s o in
       Coq_out_ter (s1, (res_val (Coq_value_object l))))
  | Coq_prim_string s0 ->
    let o2 = (object_new (Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_string_proto)) ("String")) in
    let o1 = (object_with_get_own_property o2 Coq_builtin_get_own_prop_string) in
    let o = (object_with_primitive_value o1 (Coq_value_prim (Coq_prim_string s0))) in
    let (l, s1) = object_alloc s o in
    let%some s_2 = (object_heap_map_properties_pickable_option
                      s1 l
                      (fun p ->
                         HeapStr.write p ("length")
                           (Coq_attributes_data_of
                              (attributes_data_intro_constant
                                 (Coq_value_prim
                                    (Coq_prim_number (number_of_int (strlength s0)))))))) in
    res_ter s_2 (res_val (Coq_value_object l))
  | _ ->
    (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
      s
      ("[prim_new_object] received an null or undef.")

(** val to_object : state -> value -> result **)

and to_object s _foo_ = match _foo_ with
  | Coq_value_prim w ->
    (match w with
     | Coq_prim_undef -> run_error s Coq_native_error_type
     | Coq_prim_null -> run_error s Coq_native_error_type
     | Coq_prim_bool b -> prim_new_object s w
     | Coq_prim_number n -> prim_new_object s w
     | Coq_prim_string s0 -> prim_new_object s w)
  | Coq_value_object l ->
    result_out (Coq_out_ter (s, (res_val (Coq_value_object l))))

(** val run_object_prim_value : state -> object_loc -> result **)

and run_object_prim_value s l =
  let%some ov = (run_object_method object_prim_value_ s l) in
      let%some v = (ov) in  res_ter s (res_val v)

(** val prim_value_get :
    state -> execution_ctx -> value -> prop_name -> result **)

and prim_value_get s c v x =
  let%object (s_2, l) = (to_object s v) in
      object_get_builtin s_2 c Coq_builtin_get_default v l x

(** val env_record_has_binding :
    state -> execution_ctx -> env_loc -> prop_name -> result **)

and env_record_has_binding s c l x =
  let%some e = (env_record_binds_pickable_option s l) in
      match e with
      | Coq_env_record_decl ed ->
        result_out (Coq_out_ter (s,
                                 (res_val (Coq_value_prim (Coq_prim_bool
                                                             (HeapStr.indom_dec ed x))))))
      | Coq_env_record_object (l0, pt) -> object_has_prop s c l0 x

(** val lexical_env_get_identifier_ref :
    state -> execution_ctx -> lexical_env -> prop_name ->
    strictness_flag -> ref specres **)

and lexical_env_get_identifier_ref s c x x0 str =
  match x with
  | [] ->
    res_spec s (ref_create_value (Coq_value_prim Coq_prim_undef) x0 str)
  | l :: x_2 ->
    let%bool (s1, has) = (env_record_has_binding s c l x0) in
        if has
        then res_spec s1 (ref_create_env_loc l x0 str)
        else lexical_env_get_identifier_ref s1 c x_2 x0 str

(** val object_delete_default :
    state -> execution_ctx -> object_loc -> prop_name ->
    strictness_flag -> result **)

and object_delete_default s c l x str =
  let%run (s1, d) = (run_object_get_own_prop s c l x) in
      match d with
      | Coq_full_descriptor_undef ->
        res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool true)))
      | Coq_full_descriptor_some a ->
        if attributes_configurable a
        then let%some
             s_2 = (object_heap_map_properties_pickable_option s1 l (fun p ->
                 HeapStr.rem p x)) in
                res_ter s_2 (res_val (Coq_value_prim (Coq_prim_bool true)))
        else out_error_or_cst s1 str Coq_native_error_type (Coq_value_prim
                                                              (Coq_prim_bool false))

(** val object_delete :
    state -> execution_ctx -> object_loc -> prop_name ->
    strictness_flag -> result **)

and object_delete s c l x str =
  let%some b = (run_object_method object_delete_ s l) in
      match b with
      | Coq_builtin_delete_default -> object_delete_default s c l x str
      | Coq_builtin_delete_args_obj ->
        let%some mo = (run_object_method object_parameter_map_ s l) in
            let%some m = (mo) in
                let%run (s1, d) = (run_object_get_own_prop s c m x) in
                    let%bool (s2, b0) = (object_delete_default s1 c l x str) in
                        if b0
                        then (match d with
                            | Coq_full_descriptor_undef ->
                              res_ter s2
                                (res_val (Coq_value_prim (Coq_prim_bool b0)))
                            | Coq_full_descriptor_some a ->
                              let%bool 
                                (s3, b_2) = (object_delete s2 c m x false) in
                                   res_ter s3
                                     (res_val (Coq_value_prim (Coq_prim_bool b0))))
                        else res_ter s2 (res_val (Coq_value_prim (Coq_prim_bool b0)))

(** val env_record_delete_binding :
    state -> execution_ctx -> env_loc -> prop_name -> result **)

and env_record_delete_binding s c l x =
  let%some e = (env_record_binds_pickable_option s l) in
      match e with
      | Coq_env_record_decl ed ->
        (match HeapStr.read_option ed x with
         | Some p ->
           let (mu, v) = p in
           (match mu with
            | Coq_mutability_uninitialized_immutable ->
              result_out (Coq_out_ter (s,
                                       (res_val (Coq_value_prim (Coq_prim_bool false)))))
            | Coq_mutability_immutable ->
              result_out (Coq_out_ter (s,
                                       (res_val (Coq_value_prim (Coq_prim_bool false)))))
            | Coq_mutability_nondeletable ->
              result_out (Coq_out_ter (s,
                                       (res_val (Coq_value_prim (Coq_prim_bool false)))))
            | Coq_mutability_deletable ->
              let s_2 =
                env_record_write s l (Coq_env_record_decl
                                        (decl_env_record_rem ed x))
              in
              result_out (Coq_out_ter (s_2,
                                       (res_val (Coq_value_prim (Coq_prim_bool true))))))
         | None ->
           result_out (Coq_out_ter (s,
                                    (res_val (Coq_value_prim (Coq_prim_bool true))))))
      | Coq_env_record_object (l0, pt) ->
        object_delete s c l0 x throw_false

(** val env_record_implicit_this_value : state -> env_loc -> value option **)

and env_record_implicit_this_value s l =
  ifx_some_or_default (env_record_binds_pickable_option s l) None (fun e ->
      Some
        (match e with
         | Coq_env_record_decl ed -> Coq_value_prim Coq_prim_undef
         | Coq_env_record_object (l0, provide_this) ->
           if provide_this
           then Coq_value_object l0
           else Coq_value_prim Coq_prim_undef))

(** val identifier_resolution :
    state -> execution_ctx -> prop_name -> ref specres **)

and identifier_resolution s c x =
  let x0 = c.execution_ctx_lexical_env in
  let str = c.execution_ctx_strict in
  lexical_env_get_identifier_ref s c x0 x str

(** val env_record_get_binding_value :
    state -> execution_ctx -> env_loc -> prop_name ->
    strictness_flag -> result **)

and env_record_get_binding_value s c l x str =
  let%some e = (env_record_binds_pickable_option s l) in
      match e with
      | Coq_env_record_decl ed ->
        let%some rm = (HeapStr.read_option ed x) in
            let (mu, v) = rm in
            if mutability_compare mu Coq_mutability_uninitialized_immutable
            then out_error_or_cst s str Coq_native_error_ref (Coq_value_prim
                                                                Coq_prim_undef)
            else res_ter s (res_val v)
      | Coq_env_record_object (l0, pt) ->
        let%bool (s1, has) = (object_has_prop s c l0 x) in
            if has
            then run_object_get s1 c l0 x
            else out_error_or_cst s1 str Coq_native_error_ref (Coq_value_prim
                                                                 Coq_prim_undef)

(** val ref_get_value :
    state -> execution_ctx -> resvalue -> value specres **)

and ref_get_value s c _foo_ = match _foo_ with
  | Coq_resvalue_empty ->
    (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
      s
      ("[ref_get_value] received an empty result.")
  | Coq_resvalue_value v -> res_spec s v
  | Coq_resvalue_ref r ->
    let 
      for_base_or_object = (fun tt ->
        match r.ref_base with
        | Coq_ref_base_type_value v ->
          if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_primitive_base
          then let%value (s2, v) = (prim_value_get s c v r.ref_name) in res_spec s2 v
          else (match v with
              | Coq_value_prim p ->
                (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)