[trans] Make metas appear before actual corresponding input/output variable declarations.

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