From c2482b55d1bedc8df67e833ab2b11e332c71dc7a Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 23 Mar 2023 15:11:46 +0100
Subject: [PATCH] [interpretation] Add support for theory scopes for builtins.
---
src/interpretation.ml | 18 ++---
src/reduction_engine.ml | 132 +++++++++++++++++-----------------
src/reduction_engine.mli | 2 +-
stdlib/interpretation.mlw | 3 +-
tests/interpretation_acasxu.t | 2 +-
5 files changed, 81 insertions(+), 76 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index 96f775b..df78bca 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -304,26 +304,28 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
"Vector",
[],
[
- (Ident.op_get "" (* ([]) *), None, vget);
- ("length", None, length);
- ("mapi", None, mapi);
+ ([ Ident.op_get "" ] (* ([]) *), None, vget);
+ ([ "length" ], None, length);
+ ([ "L"; "mapi" ], None, mapi);
] );
( [ "interpretation" ],
"Tensor",
[],
- [ (Ident.op_infix "#", None, tget); (Ident.op_infix "-", None, tminus) ]
- );
+ [
+ ([ Ident.op_infix "#" ], None, tget);
+ ([ Ident.op_infix "-" ], None, tminus);
+ ] );
( [ "interpretation" ],
"Classifier",
[],
[
- ("read_classifier", None, read_classifier);
- (Ident.op_infix "@@", None, apply_classifier);
+ ([ "read_classifier" ], None, read_classifier);
+ ([ Ident.op_infix "@@" ], None, apply_classifier);
] );
( [ "interpretation" ],
"Dataset",
[],
- [ ("read_dataset", None, read_dataset) ] );
+ [ ([ "read_dataset" ], None, read_dataset) ] );
]
let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index 149c4c7..f586355 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -126,37 +126,41 @@ let eval_int_op op simpl _ ls l ty =
| _ -> assert false
let simpl_add _ls t1 t2 _ty =
- Value
- (if is_zero t1 then t2 else if is_zero t2 then t1 else raise Undetermined)
+ if is_zero t1
+ then Value t2
+ else if is_zero t2
+ then Value t1
+ else raise Undetermined
let simpl_sub _ls t1 t2 _ty =
- Value (if is_zero t2 then t1 else raise Undetermined)
+ if is_zero t2 then Value t1 else raise Undetermined
let simpl_mul _ls t1 t2 _ty =
- Value
- (if is_zero t1
- then t1
- else if is_zero t2
- then t2
- else if is_one t1
- then t2
- else if is_one t2
- then t1
- else raise Undetermined)
+ if is_zero t1
+ then Value t1
+ else if is_zero t2
+ then Value t2
+ else if is_one t1
+ then Value t2
+ else if is_one t2
+ then Value t1
+ else raise Undetermined
let simpl_div _ls t1 t2 _ty =
- Value
- (if is_zero t2 then raise Undetermined;
- if is_zero t1 then t1 else if is_one t2 then t1 else raise Undetermined)
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1
+ then Value t1
+ else if is_one t2
+ then Value t1
+ else raise Undetermined
let simpl_mod _ls t1 t2 _ty =
- Value
- (if is_zero t2 then raise Undetermined;
- if is_zero t1
- then t1
- else if is_one t2
- then Int BigInt.zero
- else raise Undetermined)
+ if is_zero t2 then raise Undetermined;
+ if is_zero t1
+ then Value t1
+ else if is_one t2
+ then Value (Int BigInt.zero)
+ else raise Undetermined
let simpl_minmax _ls v1 v2 _ty =
match (v1, v2) with
@@ -284,27 +288,25 @@ let real_mul r1 r2 =
real_value ~pow2 ~pow5 s
let simpl_real_add _ls t1 t2 _ty =
- Value
- (if is_real t1 real_0
- then t2
- else if is_real t2 real_0
- then t1
- else raise Undetermined)
+ if is_real t1 real_0
+ then Value t2
+ else if is_real t2 real_0
+ then Value t1
+ else raise Undetermined
let simpl_real_sub _ls t1 t2 _ty =
if is_real t2 real_0 then Value t1 else raise Undetermined
let simpl_real_mul _ls t1 t2 _ty =
- Value
- (if is_real t1 real_0
- then t1
- else if is_real t2 real_0
- then t2
- else if is_real t1 real_1
- then t2
- else if is_real t2 real_1
- then t1
- else raise Undetermined)
+ if is_real t1 real_0
+ then Value t1
+ else if is_real t2 real_0
+ then Value t2
+ else if is_real t1 real_1
+ then Value t2
+ else if is_real t2 real_1
+ then Value t1
+ else raise Undetermined
let real_pow r1 r2 =
let open Number in
@@ -345,7 +347,7 @@ type 'a built_in_theories =
Env.pathname
* string
* (string * (Ty.tysymbol -> unit)) list
- * (string * lsymbol ref option * 'a builtin) list
+ * (string list * lsymbol ref option * 'a builtin) list
let built_in_theories : unit -> 'a built_in_theories list =
fun () ->
@@ -356,54 +358,54 @@ let built_in_theories : unit -> 'a built_in_theories list =
"Int",
[],
[
- (Ident.op_infix "+", None, eval_int_op BigInt.add simpl_add);
- (Ident.op_infix "-", None, eval_int_op BigInt.sub simpl_sub);
- (Ident.op_infix "*", None, eval_int_op BigInt.mul simpl_mul);
- (Ident.op_prefix "-", None, eval_int_uop BigInt.minus);
- (Ident.op_infix "<", None, eval_int_rel BigInt.lt);
- (Ident.op_infix "<=", None, eval_int_rel BigInt.le);
- (Ident.op_infix ">", None, eval_int_rel BigInt.gt);
- (Ident.op_infix ">=", None, eval_int_rel BigInt.ge);
+ ([ Ident.op_infix "+" ], None, eval_int_op BigInt.add simpl_add);
+ ([ Ident.op_infix "-" ], None, eval_int_op BigInt.sub simpl_sub);
+ ([ Ident.op_infix "*" ], None, eval_int_op BigInt.mul simpl_mul);
+ ([ Ident.op_prefix "-" ], None, eval_int_uop BigInt.minus);
+ ([ Ident.op_infix "<" ], None, eval_int_rel BigInt.lt);
+ ([ Ident.op_infix "<=" ], None, eval_int_rel BigInt.le);
+ ([ Ident.op_infix ">" ], None, eval_int_rel BigInt.gt);
+ ([ Ident.op_infix ">=" ], None, eval_int_rel BigInt.ge);
] );
( [ "int" ],
"MinMax",
[],
[
- ("min", None, eval_int_op BigInt.min simpl_minmax);
- ("max", None, eval_int_op BigInt.max simpl_minmax);
+ ([ "min" ], None, eval_int_op BigInt.min simpl_minmax);
+ ([ "max" ], None, eval_int_op BigInt.max simpl_minmax);
] );
( [ "int" ],
"ComputerDivision",
[],
[
- ("div", None, eval_int_op BigInt.computer_div simpl_div);
- ("mod", None, eval_int_op BigInt.computer_mod simpl_mod);
+ ([ "div" ], None, eval_int_op BigInt.computer_div simpl_div);
+ ([ "mod" ], None, eval_int_op BigInt.computer_mod simpl_mod);
] );
( [ "int" ],
"EuclideanDivision",
[],
[
- ("div", None, eval_int_op BigInt.euclidean_div simpl_div);
- ("mod", None, eval_int_op BigInt.euclidean_mod simpl_mod);
+ ([ "div" ], None, eval_int_op BigInt.euclidean_div simpl_div);
+ ([ "mod" ], None, eval_int_op BigInt.euclidean_mod simpl_mod);
] );
( [ "real" ],
"Real",
[],
[
- (Ident.op_prefix "-", None, eval_real_uop real_opp);
- (Ident.op_infix "+", None, eval_real_op real_add simpl_real_add);
- (Ident.op_infix "-", None, eval_real_op real_sub simpl_real_sub);
- (Ident.op_infix "*", None, eval_real_op real_mul simpl_real_mul);
- (Ident.op_infix "<", None, eval_real_rel BigInt.lt);
- (Ident.op_infix "<=", None, eval_real_rel BigInt.le);
- (Ident.op_infix ">", None, eval_real_rel BigInt.gt);
- (Ident.op_infix ">=", None, eval_real_rel BigInt.ge);
+ ([ Ident.op_prefix "-" ], None, eval_real_uop real_opp);
+ ([ Ident.op_infix "+" ], None, eval_real_op real_add simpl_real_add);
+ ([ Ident.op_infix "-" ], None, eval_real_op real_sub simpl_real_sub);
+ ([ Ident.op_infix "*" ], None, eval_real_op real_mul simpl_real_mul);
+ ([ Ident.op_infix "<" ], None, eval_real_rel BigInt.lt);
+ ([ Ident.op_infix "<=" ], None, eval_real_rel BigInt.le);
+ ([ Ident.op_infix ">" ], None, eval_real_rel BigInt.gt);
+ ([ Ident.op_infix ">=" ], None, eval_real_rel BigInt.ge);
] );
- ([ "real" ], "FromInt", [], [ ("from_int", None, real_from_int) ]);
+ ([ "real" ], "FromInt", [], [ ([ "from_int" ], None, real_from_int) ]);
( [ "real" ],
"PowerReal",
[],
- [ ("pow", None, eval_real_op real_pow simpl_real_pow) ] );
+ [ ([ "pow" ], None, eval_real_op real_pow simpl_real_pow) ] );
(* ["map"],"Map", ["map", builtin_map_type], [ "const", Some ls_map_const,
eval_map_const; "get", Some ls_map_get, eval_map_get; "set", Some
ls_map_set, eval_map_set; ] ; *)
@@ -418,7 +420,7 @@ let add_builtin_th env ((l, n, t, d) : 'a built_in_theories) =
t;
List.iter
(fun (id, r, f) ->
- let ls = Theory.ns_find_ls th.Theory.th_export [ id ] in
+ let ls = Theory.ns_find_ls th.Theory.th_export id in
Hls.add env.builtins ls f;
match r with None -> () | Some r -> r := ls)
d
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
index a024810..8b8dc30 100644
--- a/src/reduction_engine.mli
+++ b/src/reduction_engine.mli
@@ -101,7 +101,7 @@ type 'a built_in_theories =
Env.pathname
* string
* (string * (Ty.tysymbol -> unit)) list
- * (string * Why3.Term.lsymbol ref option * 'a builtin) list
+ * (string list * Why3.Term.lsymbol ref option * 'a builtin) list
type bounded_quant_result = {
new_quant : Term.vsymbol list;
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index 0c925d9..f22eec4 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -29,8 +29,9 @@ theory Vector
function length (v: vector 'a) : int
predicate has_length (v: vector 'a) (i: int)
- function mapi (v: vector 'a) (f: int -> 'a -> 'b) : vector 'b
+
scope L
+ function mapi (v: vector 'a) (f: int -> 'a -> 'b) : vector 'b
function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 2c8259d..4439abb 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -57,7 +57,7 @@ Test interpret on acasxu
> else t
>
> function denormalize_input (i:input) : input =
- > mapi i denormalize_by_index
+ > Vector.L.mapi i denormalize_by_index
>
> function denormalize_output (o: t) : t =
> denormalize_t o (7.51888402010059753166615337249822914600372314453125:t) (373.9499200000000200816430151462554931640625:t)
--
GitLab