[aimos] Make proper `aimos_params` type and use it

src/AIMOS.ml

@@ -88,8 +88,11 @@ let build_command config_prover
   let perturbation, (amplitude : Dataset.amplitude), perturbation_path, out_mode
       =
     match predicate.property with
-    | Dataset.MetaRobust (_, p, ctp, om, start, stop, step) ->
-      (p, { start = Some start; stop; step = Some step }, ctp, om)
+    | Dataset.MetaRobust (_, aimos_params) ->
+      ( aimos_params.perturbation,
+        aimos_params.amplitude,
+        aimos_params.ctp,
+        aimos_params.om )
     | _ -> failwith "Unsupported property"
   in
   let aimos_config =
@@ -104,7 +107,7 @@ let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
 let build_answer predicate_kind prover_result =
   let threshold =
     match predicate_kind with
-    | Dataset.MetaRobust (f, _, _, _, _, _, _) ->
+    | Dataset.MetaRobust (f, _) ->
       Float.of_string (Dataset.string_of_threshold f)
     | _ -> failwith "Unsupported property"
   in

src/dataset.ml

@@ -56,7 +56,15 @@ type amplitude = {
   stop : int;
   step : int option;
 }
-[@@deriving yojson]
+[@@deriving yojson, show]
+
+type aimos_params = {
+  perturbation : string;
+  ctp : string;
+  om : string;
+  amplitude : amplitude;
+}
+[@@deriving yojson, show]
 
 let string_of_threshold threshold = Float.to_string threshold
 
@@ -80,7 +88,7 @@ type property =
   | Correct
   | Robust of eps
   | CondRobust of eps
-  | MetaRobust of threshold * string * string * string * int * int * int
+  | MetaRobust of threshold * aimos_params
 [@@deriving yojson, show]
 
 type ('a, 'b) predicate = {
@@ -146,12 +154,17 @@ let interpret_predicate env ~on_model ~on_dataset task =
         then
           MetaRobust
             ( f,
-              p,
-              ctp,
-              om,
-              Number.to_small_integer start,
-              Number.to_small_integer stop,
-              Number.to_small_integer step )
+              {
+                perturbation = p;
+                ctp;
+                om;
+                amplitude =
+                  {
+                    start = Some (Number.to_small_integer start);
+                    stop = Number.to_small_integer stop;
+                    step = Some (Number.to_small_integer step);
+                  };
+              } )
         else failwith_unsupported_ls ls
       | _ -> failwith_unsupported_term term
     in

src/dataset.mli

@@ -35,7 +35,15 @@ type amplitude = {
   stop : int;
   step : int option;
 }
-[@@deriving yojson]
+[@@deriving yojson, show]
+
+type aimos_params = {
+  perturbation : string;
+  ctp : string;
+  om : string;
+  amplitude : amplitude;
+}
+[@@deriving yojson, show]
 
 val string_of_threshold : threshold -> string
 val string_of_amplitude : amplitude -> string option
@@ -44,7 +52,7 @@ type property = private
   | Correct
   | Robust of eps
   | CondRobust of eps
-  | MetaRobust of threshold * string * string * string * int * int * int
+  | MetaRobust of threshold * aimos_params
 [@@deriving yojson, show]
 
 type ('model, 'dataset) predicate = private {