From f75b76f8b1e7995fd7afa049e0cba4a1a6b4d52c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 15:02:48 +0100
Subject: Add an input_lvs field to Pure.fun_def

---
 src/Pure.ml           | 3 +++
 src/SymbolicToPure.ml | 5 ++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3