[interpretation] Example with forall_ predicate.

src/reduction_engine.ml

@@ -14,6 +14,8 @@ open Term
 
 [@@@ocaml.warning "-9"]
 
+let debug = Debug.register_info_flag ~desc:"" "Reduction_engine"
+
 (* {2 Values} *)
 
 type value =
@@ -1074,7 +1076,7 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
     let args = List.map term_of_value args in
     match Ident.Mid.find ls.ls_name engine.known_map with
     | exception Not_found ->
-      Format.eprintf "Reduction engine, ident not found: %s@."
+      Debug.dprintf debug "Reduction engine, ident not found: %s@."
         ls.ls_name.Ident.id_string;
       {
         value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;

stdlib/caisar.mlw

@@ -82,11 +82,13 @@ theory NN
 end
 
 theory Interpret
+  use bool.Bool
 
+  type input
   type dataset
 
   function open_dataset string: dataset
-
   function size dataset: int
 
+  predicate forall_ (d: dataset) (f: input -> bool)
 end

tests/interpretation.t

-Test verify
+Test interpret
   $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >  use caisar.Interpret
@@ -14,7 +14,11 @@ Test verify
   >       let dataset = open_dataset "datasets/a" in
   >       size dataset = 2
   > 
+  >  predicate robust (i: input)
   > 
+  >   goal G5:
+  >       let dataset = open_dataset "datasets/a" in
+  >       forall_ dataset (fun i -> robust i)
   > end
   > EOF
   G1 : true
@@ -27,3 +31,6 @@ Test verify
   G4 : true
   caisar_op1,
   (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+  G5 : forall_ caisar_op2 (fun (i:input) -> robust i)
+  caisar_op2,
+  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })