[dataset] Rename some types.

src/SAVer.ml

@@ -111,7 +111,7 @@ let call_prover limit config config_prover predicate =
     let svm = predicate.Dataset.model.Language.filename in
     let dataset = predicate.dataset in
     let eps =
-      match predicate.kind with
+      match predicate.property with
       | Dataset.Correct -> None
       | Robust e | CondRobust e -> Some e
     in
@@ -134,4 +134,4 @@ let call_prover limit config config_prover predicate =
       ~printing_info:Printer.default_printing_info (Buffer.create 10)
   in
   let prover_result = Call_provers.wait_on_call prover_call in
-  build_answer predicate.kind prover_result
+  build_answer predicate.property prover_result

src/dataset.ml

@@ -23,13 +23,13 @@
 open Why3
 open Base
 
-type feature_scaling =
+type normalization =
   | MinMax of float * float (* min-max scaling *)
   | Znorm of float * float (* z-normalization (mean, standard deviation) *)
 
 let require_clipping = function MinMax _ -> true | Znorm _ -> false
 
-let apply_feature_scaling csv ds =
+let apply_normalization csv ds =
   let transform =
     match ds with
     | MinMax (min, max) -> fun e -> (e -. min) /. (max -. min)
@@ -44,7 +44,7 @@ let apply_feature_scaling csv ds =
     in
     class_ :: features)
 
-let interpret_feature_scaling =
+let interpret_normalization =
   let float_of_real_constant rc =
     Float.of_string (Fmt.str "%a" Number.(print_real_constant full_support) rc)
   in
@@ -81,7 +81,7 @@ let interpret_feature_scaling =
 
 type eps = Constant.constant
 
-type predicate_kind =
+type property =
   | Correct
   | Robust of eps
   | CondRobust of eps
@@ -89,8 +89,8 @@ type predicate_kind =
 type ('a, 'b) predicate = {
   model : 'a;
   dataset : 'b;
-  feature_scaling : feature_scaling list;
-  kind : predicate_kind;
+  normalization : normalization list;
+  property : property;
 }
 
 let string_of_eps eps = Fmt.str "%a" Constant.print_def eps
@@ -112,7 +112,7 @@ let failwith_unsupported_ls ls =
 
 let interpret_predicate env ~on_model ~on_dataset task =
   let task = Trans.apply Introduction.introduce_premises task in
-  let feature_scaling = Trans.apply interpret_feature_scaling task in
+  let normalization = Trans.apply interpret_normalization task in
   let term = Task.task_goal_fmla task in
   match term.t_node with
   | Term.Tapp
@@ -120,7 +120,7 @@ let interpret_predicate env ~on_model ~on_dataset task =
         { t_node = Tapp (model, _); _ }
         :: { t_node = Tapp (dataset, _); _ }
         :: tt ) ->
-    let kind =
+    let property =
       match tt with
       | [] ->
         let correct_predicate = find_predicate_ls env "correct" in
@@ -139,7 +139,7 @@ let interpret_predicate env ~on_model ~on_dataset task =
     in
     let dataset = on_dataset dataset in
     let model = on_model model in
-    { model; dataset; feature_scaling; kind }
+    { model; dataset; normalization; property }
   | _ ->
     (* No other term node is supported. *)
     failwith_unsupported_term term
@@ -240,12 +240,12 @@ let add_decls ~id task n =
 let tasks_of_nn_csv_predicate env
   (predicate : (Language.nn_shape, Csv.t) predicate) =
   let clip, dataset =
-    List.fold predicate.feature_scaling ~init:(false, predicate.dataset)
+    List.fold predicate.normalization ~init:(false, predicate.dataset)
       ~f:(fun (rc, dataset) fs ->
-      (rc || require_clipping fs, apply_feature_scaling dataset fs))
+      (rc || require_clipping fs, apply_normalization dataset fs))
   in
-  let real_theory = Env.read_theory env [ "real" ] "Real" in
-  let task = Task.use_export None real_theory in
+  let th_real = Env.read_theory env [ "real" ] "Real" in
+  let task = Task.use_export None th_real in
   (* Add input declarations. *)
   let inputs, task =
     add_decls ~id:(Fmt.str "X_%d") task predicate.model.Language.nb_inputs
@@ -267,8 +267,8 @@ let tasks_of_nn_csv_predicate env
         tasks)
       else
         let task =
-          add_input_decls ~clip predicate.kind ~inputs ~record real_theory task
-          |> add_output_decl ~id predicate.kind ~outputs ~record real_theory
+          add_input_decls ~clip predicate.property ~inputs ~record th_real task
+          |> add_output_decl ~id predicate.property ~outputs ~record th_real
         in
         task :: tasks)
   in

src/dataset.mli

@@ -24,18 +24,18 @@ open Why3
 
 type eps
 
-type predicate_kind = private
+type property = private
   | Correct
   | Robust of eps
   | CondRobust of eps
 
-type feature_scaling
+type normalization
 
 type ('model, 'dataset) predicate = private {
   model : 'model;
   dataset : 'dataset;
-  feature_scaling : feature_scaling list;
-  kind : predicate_kind;
+  normalization : normalization list;
+  property : property;
 }
 
 val string_of_eps : eps -> string