From d3f7a1f2475f6bd928f2b8e8c6643725251c2d9b Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 4 Jan 2023 11:34:26 +0100
Subject: [PATCH] [language] Standardize shape type.
---
src/SAVer.ml | 2 +-
src/language.ml | 6 +++---
src/language.mli | 4 ++--
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/SAVer.ml b/src/SAVer.ml
index cc1bfc6..f5347ec 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -77,7 +77,7 @@ let re_group_number_of_predicate = function
let negative_answer = function
| Dataset.Correct ->
- (* SAVer is complete wrt correct predicate. *)
+ (* SAVer is complete wrt [Correct] predicate. *)
Call_provers.Invalid
| Robust _ | CondRobust _ -> Call_provers.Unknown ""
diff --git a/src/language.ml b/src/language.ml
index 7d7abb4..88d81e5 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -37,7 +37,7 @@ type nn_shape = {
type svm_shape = {
nb_inputs : int;
- nb_classes : int;
+ nb_outputs : int;
filename : string;
}
@@ -86,7 +86,7 @@ let register_nn_as_array env nb_inputs nb_outputs filename ?nier mstr =
in
Wstdlib.Mstr.add name (Pmodule.close_module th_uc) mstr
-let register_svm_as_array env nb_inputs nb_classes filename mstr =
+let register_svm_as_array env nb_inputs nb_outputs filename mstr =
let name = "AsArray" in
let th_uc = Pmodule.create_module env (Ident.id_fresh name) in
let svm = Pmodule.read_module env [ "caisar" ] "DatasetClassification" in
@@ -95,7 +95,7 @@ let register_svm_as_array env nb_inputs nb_classes filename mstr =
Ty.ty_app Theory.(ns_find_ts svm.mod_theory.th_export [ "model" ]) []
in
let ls_model = Term.create_fsymbol (Ident.id_fresh "model") [] svm_type in
- Term.Hls.add loaded_svms ls_model { filename; nb_inputs; nb_classes };
+ Term.Hls.add loaded_svms ls_model { filename; nb_inputs; nb_outputs };
let th_uc =
Pmodule.add_pdecl ~vc:false th_uc
(Pdecl.create_pure_decl (Decl.create_param_decl ls_model))
diff --git a/src/language.mli b/src/language.mli
index 68c7157..eb025a8 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -32,7 +32,7 @@ type nn_shape = private {
type svm_shape = private {
nb_inputs : int;
- nb_classes : int;
+ nb_outputs : int;
filename : string;
}
@@ -60,5 +60,5 @@ val onnx_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
the given onnx [filename]. The result is memoized. *)
val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
-(* [nnet_parser env filename] parses and creates the theories corresponding to
+(* [ovo_parser env filename] parses and creates the theories corresponding to
the given ovo [filename]. The result is memoized. *)
--
GitLab