From ed8c20980fbf5a28e83702cbfac20502cbca83e8 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 31 Aug 2022 18:17:21 +0200
Subject: [PATCH] [language] Some renaming and style rework.
---
src/language.ml | 10 +++++-----
src/language.mli | 12 ++++++------
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index df0d8756..bbca3a69 100644
--- a/src/language.ml
+++ b/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))
diff --git a/src/language.mli b/src/language.mli
index 110da05e..cd3329a2 100644
--- a/src/language.mli
+++ b/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. *)
--
GitLab