[interpretation] Remove scopes from library theories.

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",

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

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)

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