diff --git a/generator/monad_ppx.ml b/generator/monad_ppx.ml index 9aec6d07f0219c8f66fbe899fe1471aef79a8374..42ea9ff5591755bec8090789e7da97db459468cc 100644 --- a/generator/monad_ppx.ml +++ b/generator/monad_ppx.ml @@ -10,6 +10,7 @@ let monad_mapping = ("string", "if_string"); ("object", "if_object"); ("value", "if_value"); + ("prim", "if_prim"); (*("success", "ifsuccess")*) ] diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml index 6cb6027e50f2acf45607f5fc477147a23a13e0e9..ebf47ba366b49fa0c771ae614451b511f1b6be7d 100644 --- a/generator/tests/jsref/JsInterpreter.ml +++ b/generator/tests/jsref/JsInterpreter.ml @@ -456,8 +456,8 @@ and to_primitive s c v prefo = | Coq_value_prim w -> result_out (Coq_out_ter (s, (res_val (Coq_value_prim w)))) | Coq_value_object l -> - if_prim (object_default_value s c l prefo) (fun s0 r -> - res_ter s0 (res_val (Coq_value_prim r))) + 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 **) @@ -467,11 +467,11 @@ and to_number s c _foo_ = match _foo_ with result_out (Coq_out_ter (s, (res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w)))))) | Coq_value_object l -> - if_prim - (to_primitive s c (Coq_value_object l) (Some Coq_preftype_number)) - (fun s1 w -> + 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))))) + (res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w)))) (** val to_integer : state -> execution_ctx -> value -> result **) @@ -502,11 +502,11 @@ and to_string s c _foo_ = match _foo_ with result_out (Coq_out_ter (s, (res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w)))))) | Coq_value_object l -> - if_prim - (to_primitive s c (Coq_value_object l) (Some Coq_preftype_string)) - (fun s1 w -> + 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))))) + (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 **)