Add an input_lvs field to Pure.fun_def

2 files changed, 7 insertions, 1 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 90f6dc26..fc6cbad1 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -496,5 +496,8 @@ type fun_def = {
        *)
   signature : fun_sig;
   inputs : var list;
+  inputs_lvs : typed_lvalue list;
+      (** The inputs seen as lvalues. Allows to make transformations, for example
+          to replace unused variables by `_` *)
   body : expression;
 }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index d7bcadb4..ada64720 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1292,12 +1292,15 @@ let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
              backward_ids)
   in
   let inputs = List.append ctx.forward_inputs backward_inputs in
+  let inputs_lvs = List.map (fun v -> mk_typed_lvalue_from_var v None) inputs in
   (* Sanity check *)
   assert (
     List.for_all
       (fun (var, ty) -> (var : var).ty = ty)
       (List.combine inputs signature.inputs));
-  let def = { def_id; back_id = bid; basename; signature; inputs; body } in
+  let def =
+    { def_id; back_id = bid; basename; signature; inputs; inputs_lvs; body }
+  in
   (* Debugging *)
   log#ldebug
     (lazy