interpretation_dataset.t

Test interpret on dataset
  $ cat - > dataset.csv << EOF
  > 1,0.0,1.0,0.784313725,0.019607843,0.776470588
  > 0,1.0,0.0,0.019607843,0.776470588,0.784313725
  > EOF

  $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
  > theory T
  >   use ieee_float.Float64
  >   use bool.Bool
  >   use int.Int
  >   use interpretation.Vector
  >   use interpretation.Tensor
  >   use interpretation.Classifier
  >   use interpretation.Dataset
  > 
  >   type image = tensor t
  >   type label_ = int
  > 
  >   predicate valid_image (i: image) =
  >     forall v: index. valid_index i v -> (0.0: t) .<= i#v .<= (1.0: t)
  > 
  >   predicate valid_label (l: label_) = 0 <= l <= 1
  > 
  >   predicate advises (c: classifier) (i: image) (l: label_) =
  >     valid_label l ->
  >     forall j: int. valid_label j /\  j <> l -> (c@@i)[l] .> (c@@i)[j]
  > 
  >   predicate bounded_by_epsilon (i: image) (eps: t) =
  >     forall v: index. valid_index i v -> .- eps .<= i#v .<= eps
  > 
  >   predicate robust_around (c: classifier) (eps: t) (i: image) (l: label_) =
  >     forall perturbed_image: image.
  >       valid_image perturbed_image ->
  >       equal_shape i perturbed_image ->
  >       let p = perturbed_image - i in
  >       bounded_by_epsilon p eps ->
  >       advises c perturbed_image l
  > 
  >   predicate robust (c: classifier) (d: dataset image label_) (eps: t) =
  >     Dataset.L.forall_ d (robust_around c eps)
  > 
  >   goal G:
  >     let classifier = read_classifier "TestNetwork.nnet" NNet in
  >     let dataset = read_dataset "dataset.csv" CSV in
  >     let eps = (0.375:t) in
  >     robust classifier dataset eps
  > end
  > EOF
  G : match caisar_op[0] with
      | a, b ->
          ((fun (y2:tensor t) (y3:int) ->
             forall perturbed_image:tensor t.
              (forall v:vector int.
                valid_index perturbed_image v ->
                le (0.0:t) (perturbed_image # v) /\
                le (perturbed_image # v) (1.0:t)) ->
              equal_shape y2 perturbed_image ->
              (forall v:vector int.
                valid_index (perturbed_image - y2) v ->
                le (neg (0.375:t)) ((perturbed_image - y2) # v) /\
                le ((perturbed_image - y2) # v) (0.375:t)) ->
              (0 < y3 \/ 0 = y3) /\ (y3 < 1 \/ y3 = 1) ->
              (forall j:int.
                ((0 < j \/ 0 = j) /\ (j < 1 \/ j = 1)) /\ not j = y3 ->
                lt
                (read_classifier ("TestNetwork.nnet":string) NNet
                 @@ perturbed_image)
                [j]
                (read_classifier ("TestNetwork.nnet":string) NNet