From ad2f7fc03910c330d11bd03c2afd8e60a25bae8b Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 2 May 2023 17:55:04 +0200
Subject: [PATCH] [language] Do not use type alias as type inference becomes
confused.
---
src/interpretation.ml | 6 +++---
src/language.ml | 4 ----
src/language.mli | 18 +++++++-----------
3 files changed, 10 insertions(+), 18 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index 605e68d..15f367d 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -25,13 +25,13 @@ open Why3
open Base
type classifier =
- | NNet of Language.nn_classifier
+ | NNet of Term.lsymbol
[@printer
fun fmt nn ->
Fmt.pf fmt "NNet: %a"
Fmt.(option Language.pp_nn)
(Language.lookup_nn_classifier nn)]
- | ONNX of Language.nn_classifier
+ | ONNX of Term.lsymbol
[@printer
fun fmt nn ->
Fmt.pf fmt "ONNX: %a"
@@ -45,7 +45,7 @@ type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
type data = D_csv of string list [@@deriving show]
type vector =
- (Language.vector
+ (Term.lsymbol
[@printer
fun fmt v ->
Fmt.pf fmt "%a" Fmt.(option ~none:nop int) (Language.lookup_vector v)])
diff --git a/src/language.ml b/src/language.ml
index 75a9dac..3c7db41 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -158,8 +158,6 @@ let register_ovo_support () =
(* -- Vector *)
-type vector = Term.lsymbol
-
let vectors = Term.Hls.create 10
let vector_elt_ty env =
@@ -196,8 +194,6 @@ type nn = {
}
[@@deriving show]
-type nn_classifier = Term.lsymbol
-
let nn_classifiers = Term.Hls.create 10
let fresh_classifier_ls env name =
diff --git a/src/language.mli b/src/language.mli
index 52ed49a..4ac58bc 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -65,11 +65,9 @@ val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
(** -- Vector *)
-type vector = Term.lsymbol
-
-val create_vector : Env.env -> int -> vector
-val lookup_vector : vector -> int option
-val mem_vector : vector -> bool
+val create_vector : Env.env -> int -> Term.lsymbol
+val lookup_vector : Term.lsymbol -> int option
+val mem_vector : Term.lsymbol -> bool
(** -- Classifier *)
@@ -82,9 +80,7 @@ type nn = private {
}
[@@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
+val create_nnet_classifier : Env.env -> string -> Term.lsymbol
+val create_onnx_classifier : Env.env -> string -> Term.lsymbol
+val lookup_nn_classifier : Term.lsymbol -> nn option
+val mem_nn_classifier : Term.lsymbol -> bool
--
GitLab