[interpretation] CSV dataset types comply with the particular CSV dataset format.

src/interpretation.ml

@@ -127,6 +127,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
   let error_message ls =
     Fmt.str "Invalid arguments for '%a'" Pretty.print_ls ls
   in
+
   (* Vector *)
   let vget : _ CRE.builtin =
    fun engine ls vl ty ->
@@ -146,14 +147,14 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
         in
         let ty_features =
           match ty with
-          | Some { ty_node = Tyapp (_, [ ty; _ ]); _ } -> Some ty
+          | Some { ty_node = Tyapp (_, [ _; ty ]); _ } -> Some ty
           | _ -> assert false
         in
         let t_features, t_label =
           ( term_of_caisar_op engine (Data (D_csv features)) ty_features,
             Term.t_int_const (BigInt.of_int (Int.of_string label)) )
         in
-        value_term (Term.t_tuple [ t_features; t_label ])
+        value_term (Term.t_tuple [ t_label; t_features ])
       | Vector v ->
         let n = Option.value_exn (Language.lookup_vector v) in
         assert (List.length tl1 = n && i <= n);

src/language.ml

@@ -272,7 +272,7 @@ let fresh_dataset_csv_ls env name =
     let th = Env.read_theory env [ "interpretation" ] "Dataset" in
     Ty.ty_app
       (Theory.ns_find_ts th.th_export [ "dataset" ])
-      [ ty_elt; Ty.ty_int ]
+      [ Ty.ty_int; ty_elt ]
   in
   let id = Ident.id_fresh name in
   Term.create_fsymbol id [] ty

tests/interpretation_dataset.t

@@ -14,7 +14,6 @@ Test interpret on dataset
   $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
-  >   use bool.Bool
   >   use int.Int
   >   use interpretation.Vector
   >   use interpretation.NeuralNetwork
@@ -35,7 +34,7 @@ Test interpret on dataset
   >   predicate bounded_by_epsilon (i: image) (eps: t) =
   >     forall v: index. valid_index i v -> .- eps .<= i[v] .<= eps
   > 
-  >   predicate robust_around (n: nn) (eps: t) (i: image) (l: label_) =
+  >   predicate robust_around (n: nn) (eps: t) (l: label_) (i: image) =
   >     forall perturbed_image: image.
   >       has_length perturbed_image (length i) ->
   >       valid_image perturbed_image ->
@@ -43,7 +42,7 @@ Test interpret on dataset
   >       bounded_by_epsilon perturbation eps ->
   >       advises n perturbed_image l
   > 
-  >   predicate robust (n: nn) (d: dataset image label_) (eps: t) =
+  >   predicate robust (n: nn) (d: dataset label_ image) (eps: t) =
   >     Dataset.forall_ d (robust_around n eps)
   > 
   >   goal G: