[language] Some renaming and style rework.

src/language.ml

@@ -27,14 +27,14 @@ open Base
 (* - NNet and ONNX for neural networks *)
 (* - OVO for for SVM *)
 
-type nnshape = {
+type nn_shape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
   filename : string;
 }
 
-type svmshape = { nb_inputs : int; nb_classes : int; filename : string }
+type svm_shape = { nb_inputs : int; nb_classes : int; filename : string }
 
 let loaded_nets = Term.Hls.create 10
 let loaded_svms = Term.Hls.create 10
@@ -43,21 +43,21 @@ let lookup_loaded_svms = Term.Hls.find_opt loaded_svms
 
 let register_nn_as_tuple nb_inputs nb_outputs filename env =
   let net = Pmodule.read_module env [ "caisar" ] "NN" in
-  let ioshape_input_type =
+  let input_type =
     Ty.ty_app Theory.(ns_find_ts net.mod_theory.th_export [ "input_type" ]) []
   in
   let id_as_tuple = Ident.id_fresh "NNasTuple" in
   let th_uc = Pmodule.create_module env id_as_tuple in
   let th_uc = Pmodule.use_export th_uc net in
   let ls_net_apply =
-    let f _ = ioshape_input_type in
+    let f _ = input_type in
     Term.create_fsymbol
       (Ident.id_fresh "net_apply")
       (List.init nb_inputs ~f)
       (Ty.ty_tuple (List.init nb_outputs ~f))
   in
   Term.Hls.add loaded_nets ls_net_apply
-    { filename; nb_inputs; nb_outputs; ty_data = ioshape_input_type };
+    { filename; nb_inputs; nb_outputs; ty_data = input_type };
   let th_uc =
     Pmodule.add_pdecl ~vc:false th_uc
       (Pdecl.create_pure_decl (Decl.create_param_decl ls_net_apply))

src/language.mli

@@ -22,20 +22,20 @@
 
 open Why3
 
-type nnshape = {
+type nn_shape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
   filename : string;
 }
 
-type svmshape = { nb_inputs : int; nb_classes : int; filename : string }
+type svm_shape = { nb_inputs : int; nb_classes : int; filename : string }
 
-val lookup_loaded_nets : Term.lsymbol -> nnshape option
-(** @return the filename of a nnet Why3 representation. *)
+val lookup_loaded_nets : Term.lsymbol -> nn_shape option
+(** @return the shape of a nnet Why3 representation. *)
 
-val lookup_loaded_svms : Why3.Term.lsymbol -> svmshape option
-(** @return the svmshape of a svm Why3 representation. *)
+val lookup_loaded_svms : Term.lsymbol -> svm_shape option
+(** @return the shape of a svm Why3 representation. *)
 
 val register_nnet_support : unit -> unit
 (** Register NNet parser. *)