interpretation.t

Test interpret
  $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
  > theory T
  >  use caisar.Interpretation
  >  use int.Int
  > 
  >   goal G1: 1+1=2
  > 
  >   goal G2: 1+1=3
  > 
  >   goal G3: size (open_dataset "datasets/a") = 2
  > 
  >   goal G4:
  >       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)
  > 
  >   goal G6:
  >       let dataset = open_dataset "datasets/a" in
  >       forall i:int. i=1+(size dataset) -> i < 4
  > end
  > EOF
  G1 : true
  
  G2 : false
  
  G3 : true
  caisar_op,
  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
  G4 : true
  caisar_op1,
  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
  G5 : robust (get 0 caisar_op2) /\ robust (get 1 caisar_op2)
  caisar_op2,
  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
  G6 : forall i:int. i = 3 -> i < 4
  caisar_op3,
  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })