language.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2022                                                    *)
(*    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. *)

(** -- Vector *)

type vector = Term.lsymbol

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

(** -- Classifier *)

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

type nn_classifier = Term.lsymbol

val create_nnet_classifier : Env.env -> string -> nn_classifier
val create_onnx_classifier : Env.env -> string -> nn_classifier
val lookup_nn_classifier : nn_classifier -> nn option
val mem_nn_classifier : nn_classifier -> bool