summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml
diff options
context:
space:
mode:
authorSon Ho2022-05-01 16:24:31 +0200
committerSon Ho2022-05-01 16:24:31 +0200
commitcfa016923779d681e639634b7e0dd16e1be9f003 (patch)
treee58c7d96d14562e9dff454bac6af8933e1c5b153 /src/SymbolicToPure.ml
parentb664a5b1e4814a1f0105b76d5b5265e095200c3d (diff)
Do more cleanup
Diffstat (limited to '')
-rw-r--r--src/SymbolicToPure.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index c0e47ca7..156d5661 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1019,14 +1019,14 @@ and translate_panic (config : config) (ctx : bs_ctx) : texpression =
if config.use_state_monad then
(* Create the `Fail` value *)
let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; ctx.ret_ty ] in
- let ret_v = mk_result_fail_rvalue ret_ty in
+ let ret_v = mk_result_fail_texpression ret_ty in
(* Add the lambda *)
let _, state_var =
fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
in
let state_pattern = mk_typed_pattern_from_var state_var None in
mk_abs state_pattern ret_v
- else mk_result_fail_rvalue ctx.ret_ty
+ else mk_result_fail_texpression ctx.ret_ty
and translate_return (config : config) (opt_v : V.typed_value option)
(ctx : bs_ctx) : texpression =
@@ -1051,12 +1051,12 @@ and translate_return (config : config) (opt_v : V.typed_value option)
in
let state_rvalue = mk_texpression_from_var state_var in
let ret_v =
- mk_result_return_rvalue
+ mk_result_return_texpression
(mk_simpl_tuple_texpression [ state_rvalue; v ])
in
let state_var = mk_typed_pattern_from_var state_var None in
mk_abs state_var ret_v
- else mk_result_return_rvalue v
+ else mk_result_return_texpression v
| Some bid ->
(* Backward function *)
(* Sanity check *)
@@ -1075,14 +1075,14 @@ and translate_return (config : config) (opt_v : V.typed_value option)
let state_rvalue = mk_texpression_from_var state_var in
let ret_value = mk_simpl_tuple_texpression field_values in
let ret_value =
- mk_result_return_rvalue
+ mk_result_return_texpression
(mk_simpl_tuple_texpression [ state_rvalue; ret_value ])
in
let state_var = mk_typed_pattern_from_var state_var None in
mk_abs state_var ret_value
else
let ret_value = mk_simpl_tuple_texpression field_values in
- let ret_value = mk_result_return_rvalue ret_value in
+ let ret_value = mk_result_return_texpression ret_value in
ret_value
and translate_function_call (config : config) (call : S.call) (e : S.expression)