From a88e69ddd0fc6c48321489042d3b8ac9ba911d27 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 12 May 2023 14:49:32 +0200
Subject: [PATCH] [interpretation] Remove scopes from library theories.
---
src/interpretation.ml | 2 +-
stdlib/interpretation.mlw | 34 +++++++++++++++-------------------
tests/interpretation_acasxu.t | 2 +-
tests/interpretation_dataset.t | 2 +-
4 files changed, 18 insertions(+), 22 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index d5adc15..8aa6b79 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -297,7 +297,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
([ Ident.op_get "" ] (* ([]) *), None, vget);
([ Ident.op_infix "-" ], None, vminus);
([ "length" ], None, length);
- ([ "L"; "mapi" ], None, mapi);
+ ([ "mapi" ], None, mapi);
] );
( [ "interpretation" ],
"NeuralNetwork",
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index 603276e..68a0d70 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -33,23 +33,21 @@ theory Vector
predicate has_length (v: vector 'a) (i: int)
predicate valid_index (v: vector 'a) (i: index) = 0 <= i < length v
- scope L
- function mapi (v: vector 'a) (f: index -> '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
+ function mapi (v: vector 'a) (f: index -> '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
- predicate forall_ (v: vector 'a) (f: 'a -> bool) =
- forall i: index. valid_index v i -> f v[i]
+ predicate forall_ (v: vector 'a) (f: 'a -> bool) =
+ forall i: index. valid_index v i -> f v[i]
- predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
- length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
+ predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
+ length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
- function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
- map v f
+ function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
+ map v f
- function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
- map2 v1 v2 f
- end
+ function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
+ map2 v1 v2 f
end
theory NeuralNetwork
@@ -70,11 +68,9 @@ theory Dataset
function read_dataset (f: string) (k: format) : dataset 'a 'b
- scope L
- predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
- Vector.L.forall_ d (fun e -> let a, b = e in f a b)
+ predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
+ Vector.forall_ d (fun e -> let a, b = e in f a b)
- function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
- Vector.L.foreach d (fun e -> let a, b = e in f a b)
- end
+ function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
+ Vector.foreach d (fun e -> let a, b = e in f a b)
end
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index be3de19..8591192 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -65,7 +65,7 @@ Test interpret on acasxu
> else t
>
> function denormalize_input (i:input) : input =
- > Vector.L.mapi i denormalize_by_index
+ > Vector.mapi i denormalize_by_index
>
> function denormalize_output (o: t) : t =
> denormalize_t o (7.51888402010059753166615337249822914600372314453125:t) (373.9499200000000200816430151462554931640625:t)
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index cf06a9b..9996b45 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -44,7 +44,7 @@ Test interpret on dataset
> advises n perturbed_image l
>
> predicate robust (n: nn) (d: dataset image label_) (eps: t) =
- > Dataset.L.forall_ d (robust_around n eps)
+ > Dataset.forall_ d (robust_around n eps)
>
> goal G:
> let nn = read_neural_network "TestNetwork.nnet" NNet in
--
GitLab