summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml
diff options
context:
space:
mode:
authorSon Ho2024-04-11 20:31:16 +0200
committerSon Ho2024-04-11 20:31:16 +0200
commitb6421bc01df278f625a8c95b4ea36ad2e4355718 (patch)
tree6246ef2b038560e3deae41e4fa700f14390cd14f /compiler/PureMicroPasses.ml
parent44065f447dc3a2f4b1441b97b9687d1c1b85afbf (diff)
parent2f8aa9b47acb5c98aed91c29b04f71099452e781 (diff)
Merge branch 'son/clean' into checked-ops
Diffstat (limited to '')
-rw-r--r--compiler/PureMicroPasses.ml25
1 files changed, 13 insertions, 12 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..004ecfef 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| StructUpdate supd -> update_struct_update supd ctx
| Lambda (lb, e) -> update_lambda lb e ctx
| Meta (meta, e) -> update_emeta meta e ctx
+ | EError (meta, msg) -> (ctx, EError (meta, msg))
in
(ctx, { e; ty })
(* *)
@@ -751,7 +752,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
@@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
match e with
| Var _ | CVar _ | Const _ | App _ | Qualif _
| Meta (_, _)
- | StructUpdate _ | Lambda _ ->
+ | StructUpdate _ | Lambda _
+ | EError (_, _) ->
super#visit_expression env e
| Switch (scrut, switch) -> (
match switch with
@@ -1082,19 +1084,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 +1152,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 +1791,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 +1854,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 +1892,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 =