From 54db081edaf92e307f2014b9aa5f951ad9b076e3 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 24 May 2023 15:34:58 +0200
Subject: [PATCH] [trans] Make metas appear before actual corresponding
input/output variable declarations.
---
src/transformations/native_nn_prover.ml | 28 +++++++++++++++++--------
1 file changed, 19 insertions(+), 9 deletions(-)
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 8f72180..8a3816f 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -102,23 +102,33 @@ let simplify_goal _env input_variables =
(fun task_hd acc ->
match task_hd.task_decl.td_node with
| Use _ | Clone _ | Meta _ -> Task.add_tdecl acc task_hd.task_decl
- | Decl { d_node = Dparam ls; _ } -> (
- let task = Task.add_tdecl acc task_hd.task_decl in
- match Term.Mls.find_opt ls input_variables with
- | None -> task
- | Some pos -> Task.add_meta task Utils.meta_input [ MAls ls; MAint pos ]
- )
+ | Decl { d_node = Dparam ls; _ } ->
+ (* Add the meta first, then the actual input variable declaration.
+
+ This is mandatory for allowing some printers to properly work. Such
+ printers need to collect metas and print the actual declarations if a
+ corresponding meta has been already collected. Hence metas must
+ appear before corresponding declarations. *)
+ let acc =
+ match Term.Mls.find_opt ls input_variables with
+ | None -> acc
+ | Some pos ->
+ Task.add_meta acc Utils.meta_input [ MAls ls; MAint pos ]
+ in
+ Task.add_tdecl acc task_hd.task_decl
| Decl decl ->
let decl = Decl.decl_map (fun term -> aux htbl term) decl in
let acc =
Hashtbl.fold htbl ~init:acc ~f:(fun ~key ~data acc ->
let acc = Task.add_meta acc Utils.meta_nn_filename [ MAstr key ] in
Hashtbl.fold data ~init:acc ~f:(fun ~key ~data acc ->
+ (* Add the meta first, then the actual output variable
+ declaration. Same reason as for input variable declarations. *)
let acc =
- let decl = Decl.create_param_decl data in
- Task.add_decl acc decl
+ Task.add_meta acc Utils.meta_output [ MAls data; MAint key ]
in
- Task.add_meta acc Utils.meta_output [ MAls data; MAint key ]))
+ let decl = Decl.create_param_decl data in
+ Task.add_decl acc decl))
in
Task.add_decl acc decl)
None
--
GitLab