summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml6
-rw-r--r--compiler/ExtractBase.ml8
-rw-r--r--compiler/PrintPure.ml4
-rw-r--r--compiler/Pure.ml2
-rw-r--r--compiler/PureMicroPasses.ml21
-rw-r--r--compiler/PureTypeCheck.ml2
-rw-r--r--compiler/PureUtils.ml14
-rw-r--r--compiler/SymbolicToPure.ml7
8 files changed, 30 insertions, 34 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..27e9a62c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2853,7 +2853,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| Coq ->
@@ -2884,11 +2884,11 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "==";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| HOL4 ->
- F.pp_print_string fmt "val _ = assert_return (";
+ F.pp_print_string fmt "val _ = assert_ok (";
F.pp_print_string fmt "“";
let fun_name =
ctx_get_local_function def.meta def.def_id def.loop_id ctx
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ce8c38ba..8b17591e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1020,7 +1020,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
| FStar ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail");
(TError, error_failure_id, "Failure");
(TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1029,7 +1029,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| Coq ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail_");
(TError, error_failure_id, "Failure");
(TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1038,7 +1038,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| Lean ->
[
- (TResult, result_return_id, "Result.ret");
+ (TResult, result_ok_id, "Result.ok");
(TResult, result_fail_id, "Result.fail");
(* For panic: we omit the prefix "Error." because the type is always
clear from the context. Also, "Error" is often used by user-defined
@@ -1049,7 +1049,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| HOL4 ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail");
(TError, error_failure_id, "Failure");
(* No Fuel::Zero on purpose *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..43ec083e 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -311,7 +311,7 @@ let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
| TResult ->
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then "@Result::Return"
+ if variant_id = result_ok_id then "@Result::Return"
else if variant_id = result_fail_id then "@Result::Fail"
else
craise_opt_meta __FILE__ __LINE__ meta
@@ -394,7 +394,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
| TResult ->
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then
+ if variant_id = result_ok_id then
match field_values with
| [ v ] -> "@Result::Return " ^ v
| _ ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 7de7e0f4..daf213cf 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -92,7 +92,7 @@ type assumed_ty =
(* TODO: we should never directly manipulate [Return] and [Fail], but rather
* the monadic functions [return] and [fail] (makes treatment of error and
* state-error monads more uniform) *)
-let result_return_id = VariantId.of_int 0
+let result_ok_id = VariantId.of_int 0
let result_fail_id = VariantId.of_int 1
let option_some_id = T.option_some_id
let option_none_id = T.option_none_id
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..b1c85d61 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -751,7 +751,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
},
x ) ->
(* return/fail case *)
- if variant_id = result_return_id then
+ if variant_id = result_ok_id then
(* Return case - note that the simplification we just perform
might have unlocked the tuple simplification below *)
self#visit_Let env false lv x next
@@ -1082,19 +1082,19 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let body = { body with body = body_exp; inputs_lvs } in
{ def with body = Some body }
-(** Simplify the lets immediately followed by a return.
+(** Simplify the lets immediately followed by an ok.
Ex.:
{[
x <-- f y;
- Return x
+ Ok x
~~>
f y
]}
*)
-let simplify_let_then_return _ctx (def : fun_decl) =
+let simplify_let_then_ok _ctx (def : fun_decl) =
(* Match a pattern and an expression: evaluates to [true] if the expression
is actually exactly the pattern *)
let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool
@@ -1150,7 +1150,7 @@ let simplify_let_then_return _ctx (def : fun_decl) =
| Some e ->
if match_pattern_and_expr lv e then
(* We need to wrap the right-value in a ret *)
- (mk_result_return_texpression def.meta rv).e
+ (mk_result_ok_texpression def.meta rv).e
else not_simpl_e
| None ->
if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1789,7 +1789,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let err_v = mk_texpression_from_var err_var in
let fail_value = mk_result_fail_texpression def.meta err_v e.ty in
let fail_branch = { pat = fail_pat; branch = fail_value } in
- let success_pat = mk_result_return_pattern lv in
+ let success_pat = mk_result_ok_pattern lv in
let success_branch = { pat = success_pat; branch = e } in
let switch_body = Match [ fail_branch; success_branch ] in
let e = Switch (re, switch_body) in
@@ -1852,9 +1852,9 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
f y
]}
*)
- let def = simplify_let_then_return ctx def in
+ let def = simplify_let_then_ok ctx def in
log#ldebug
- (lazy ("simplify_let_then_return:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+ (lazy ("simplify_let_then_ok:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
(* Simplify the aggregated ADTs.
@@ -1890,11 +1890,10 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* Simplify the let-then return again (the lambda simplification may have
unlocked more simplifications here) *)
- let def = simplify_let_then_return ctx def in
+ let def = simplify_let_then_ok ctx def in
log#ldebug
(lazy
- ("simplify_let_then_return (pass 2):\n\n" ^ fun_decl_to_string ctx def
- ^ "\n"));
+ ("simplify_let_then_ok (pass 2):\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
(* Decompose the monadic let-bindings - used by Coq *)
let def =
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..9eed76b2 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -32,7 +32,7 @@ let get_adt_field_types (meta : Meta.meta)
| TResult ->
let ty = Collections.List.to_cons_nil generics.types in
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then [ ty ]
+ if variant_id = result_ok_id then [ ty ]
else if variant_id = result_fail_id then [ mk_error_ty ]
else
craise __FILE__ __LINE__ meta
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6f44bb74..e8f2d95e 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -583,12 +583,12 @@ let mk_result_fail_texpression_with_error_id (meta : Meta.meta)
let error = mk_error error in
mk_result_fail_texpression meta error ty
-let mk_result_return_texpression (meta : Meta.meta) (v : texpression) :
- texpression =
+let mk_result_ok_texpression (meta : Meta.meta) (v : texpression) : texpression
+ =
let type_args = [ v.ty ] in
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
let id =
- AdtCons { adt_id = TAssumed TResult; variant_id = Some result_return_id }
+ AdtCons { adt_id = TAssumed TResult; variant_id = Some result_ok_id }
in
let qualif = { id; generics = mk_generic_args_from_types type_args } in
let cons_e = Qualif qualif in
@@ -610,11 +610,9 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern =
let error_pat : pattern = PatDummy in
mk_result_fail_pattern error_pat ty
-let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
+let mk_result_ok_pattern (v : typed_pattern) : typed_pattern =
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ v.ty ]) in
- let value =
- PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
- in
+ let value = PatAdt { variant_id = Some result_ok_id; field_values = [ v ] } in
{ value; ty }
let opt_unmeta_mplace (e : texpression) : mplace option * texpression =
@@ -788,6 +786,6 @@ let opt_destruct_ret (e : texpression) : texpression option =
ty = _;
},
arg )
- when variant_id = Some result_return_id ->
+ when variant_id = Some result_ok_id ->
Some arg
| _ -> None
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5cd13072..38ee5df1 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2102,7 +2102,7 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
else output
in
(* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
- mk_result_return_texpression ctx.meta output
+ mk_result_ok_texpression ctx.meta output
and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
(ctx : bs_ctx) : texpression =
@@ -2150,8 +2150,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
else output
in
(* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
- mk_emeta (Tag "return_with_loop")
- (mk_result_return_texpression ctx.meta output)
+ mk_emeta (Tag "return_with_loop") (mk_result_ok_texpression ctx.meta output)
and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
texpression =
@@ -3226,7 +3225,7 @@ and translate_forward_end (ectx : C.eval_ctx)
let state_var = List.map mk_texpression_from_var state_var in
let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in
- let ret = mk_result_return_texpression ctx.meta ret in
+ let ret = mk_result_ok_texpression ctx.meta ret in
(* Introduce all the let-bindings *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 19:32:01 +0000