language.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2023                                                    *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  You can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Why3

type nn_shape = private {
  nb_inputs : int;
  nb_outputs : int;
  ty_data : Ty.ty;
  filename : string;
  nier : Onnx.G.t option;
}

type svm_shape = private {
  nb_inputs : int;
  nb_outputs : int;
  filename : string;
}

val lookup_loaded_nets : Term.lsymbol -> nn_shape option
(** @return the shape of a NN given its Why3 representation. *)

val lookup_loaded_svms : Term.lsymbol -> svm_shape option
(** @return the shape of a SVM given its Why3 representation. *)

val register_nnet_support : unit -> unit
(** Register NNet parser. *)

val register_onnx_support : unit -> unit
(** Register ONNX parser. *)

val register_ovo_support : unit -> unit
(** Register OVO parser. *)

val nnet_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
(* [nnet_parser env filename] parses and creates the theories corresponding to
   the given nnet [filename]. The result is memoized. *)

val onnx_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
(* [onnx_parser env filename] parses and creates the theories corresponding to
   the given onnx [filename]. The result is memoized. *)

val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
(* [ovo_parser env filename] parses and creates the theories corresponding to
   the given ovo [filename]. The result is memoized. *)

(** {2 Vectors} *)

val create_vector : Env.env -> int -> Term.lsymbol
val lookup_vector : Term.lsymbol -> int option
val mem_vector : Term.lsymbol -> bool

(** {2 Neural Networks} *)

type nn = private {
  nn_nb_inputs : int;
  nn_nb_outputs : int;
  nn_ty_elt : Ty.ty;
  nn_filename : string;
  nn_nier : Onnx.G.t option;
}
[@@deriving show]

val create_nn_nnet : Env.env -> string -> Term.lsymbol
val create_nn_onnx : Env.env -> string -> Term.lsymbol
val lookup_nn : Term.lsymbol -> nn option
val mem_nn : Term.lsymbol -> bool
val iter_nn : (Term.lsymbol -> nn -> unit) -> unit

(** {2 Datasets} *)

type dataset = private CSV of string [@@deriving show]

val create_dataset_csv : Env.env -> string -> Term.lsymbol
val lookup_dataset_csv : Term.lsymbol -> dataset option
val mem_dataset_csv : Term.lsymbol -> bool