summaryrefslogtreecommitdiff
path: root/compiler/PureMicroPasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PureMicroPasses.ml')
-rw-r--r--compiler/PureMicroPasses.ml52
1 files changed, 51 insertions, 1 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b0cba250..8b95f729 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1498,6 +1498,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
is_local = def.is_local;
span = loop.span;
kind = def.kind;
+ backend_attributes = def.backend_attributes;
num_loops;
loop_id = Some loop.loop_id;
llbc_name = def.llbc_name;
@@ -2277,6 +2278,52 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
(* Return *)
transl
+(** Update the [reducible] attribute.
+
+ For now we mark a function as reducible when its body is only a call to a loop
+ function. This situation often happens for simple functions whose body contains
+ a loop: we introduce an intermediate function for the loop body, and the
+ translation of the function itself simply calls the loop body. By marking
+ the function as reducible, we allow tactics like [simp] or [progress] to
+ see through the definition.
+ *)
+let compute_reducible (_ctx : trans_ctx) (transl : pure_fun_translation list) :
+ pure_fun_translation list =
+ let update_one (trans : pure_fun_translation) : pure_fun_translation =
+ match trans.f.body with
+ | None -> trans
+ | Some body -> (
+ (* Check if the body is exactly a call to a loop function.
+ Note that we check that the arguments are exactly the input
+ variables - otherwise we may not want the call to be reducible;
+ for instance when using the [progress] tactic we might want to
+ use a more specialized specification theorem. *)
+ let app, args = destruct_apps body.body in
+ match app.e with
+ | Qualif
+ {
+ id = FunOrOp (Fun (FromLlbc (FunId fid, Some _lp_id)));
+ generics = _;
+ }
+ when fid = FRegular trans.f.def_id ->
+ if
+ List.length body.inputs = List.length args
+ && List.for_all
+ (fun ((var, arg) : var * texpression) ->
+ match arg.e with
+ | Var var_id -> var_id = var.id
+ | _ -> false)
+ (List.combine body.inputs args)
+ then
+ let f =
+ { trans.f with backend_attributes = { reducible = true } }
+ in
+ { trans with f }
+ else trans
+ | _ -> trans)
+ in
+ List.map update_one transl
+
(** Apply all the micro-passes to a function.
As loops are initially directly integrated into the function definition,
@@ -2337,4 +2384,7 @@ let apply_passes_to_pure_fun_translations (ctx : trans_ctx)
(* Filter the useless inputs in the loop functions (loops are initially
parameterized by *all* the symbolic values in the context, because
they may access any of them). *)
- filter_loop_inputs ctx transl
+ let transl = filter_loop_inputs ctx transl in
+
+ (* Update the "reducible" attribute *)
+ compute_reducible ctx transl