From b8848af1d69ba3f7d91a4b05dc2d92bebc4e3c58 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 17 Jan 2023 14:32:23 +0100
Subject: [PATCH] [interpretation] Example with forall_ predicate.
---
src/reduction_engine.ml | 4 +++-
stdlib/caisar.mlw | 4 +++-
tests/interpretation.t | 9 ++++++++-
3 files changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index 5b89f9f..cba302c 100644
--- a/src/reduction_engine.ml
+++ b/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;
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index b26ab6d..4e0f43e 100644
--- a/stdlib/caisar.mlw
+++ b/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
diff --git a/tests/interpretation.t b/tests/interpretation.t
index 3556e8f..409cc92 100644
--- a/tests/interpretation.t
+++ b/tests/interpretation.t
@@ -1,4 +1,4 @@
-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" })
--
GitLab