[language] Do not use type alias as type inference becomes confused.

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)])

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 =

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