summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-28 15:02:48 +0100
committerSon Ho2022-01-28 15:02:48 +0100
commitf75b76f8b1e7995fd7afa049e0cba4a1a6b4d52c (patch)
tree37a5b604d9c632dcc93e18c4e8dcc17341851b29
parent269a80fa8e87ee41948a65a168fe24ad8f388749 (diff)
Add an input_lvs field to Pure.fun_def
-rw-r--r--src/Pure.ml3
-rw-r--r--src/SymbolicToPure.ml5
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