[NN_prover] Some documentation

src/transformations/native_nn_prover.ml

@@ -29,11 +29,6 @@ type new_output = {
   term : Why3.Term.term;
 }
 
-(** invariant:
-
-    - input_vars from 0 to its length - 1
-    - outputs from length - 1 to 0 *)
-
 exception UnknownLogicSymbol
 
 let create_new_nn env input_vars outputs : string =
@@ -51,6 +46,8 @@ let create_new_nn env input_vars outputs : string =
       Ir.Nier_simple.Node.gather_int input i)
   in
   let cache = Why3.Term.Hterm.create 17 in
+  (* Instantiate the input of [old_nn] with the [old_nn_args] terms transformed
+     into node *)
   let rec convert_old_nn (old_nn : Language.nn) old_index old_nn_args :
     IR.GFloat.Node.t =
     let old_index = Why3.Number.to_small_integer old_index in
@@ -64,7 +61,9 @@ let create_new_nn env input_vars outputs : string =
           m "No parsed NN for '%s': %s" old_nn.nn_filename s)
       | Ok { nier = Ok g; _ } -> g
     in
+    (* Create the graph to replace the old input of the nn *)
     let input () =
+      (* Regroup the terms into one node *)
       let node =
         IR.Node.create
           (Concat { inputs = List.map ~f:convert_term old_nn_args; axis = 0 })
@@ -190,6 +189,7 @@ let create_new_nn env input_vars outputs : string =
   Onnx.Simple.write nn filename;
   filename
 
+(* Choose when to start the conversion to ONNX *)
 let heuristic th_model th_nn term =
   match term.Why3.Term.t_node with
   | Tapp