[interpretation] Interpret size of a dataset.

src/interpretation.ml

@@ -25,12 +25,13 @@ open Why3
 open Base
 
 type dataset = { dataset : string } [@@deriving show]
-type caisar_op = Dataset of dataset | Size of dataset [@@deriving show]
+type caisar_op = Dataset of dataset [@@deriving show]
 
 type caisar_env = {
   dataset_ty : Ty.ty;
   caisar_op_of_ls : caisar_op Term.Hls.t;
   ls_of_caisar_op : (caisar_op, Term.lsymbol) Hashtbl.t;
+  cwd : string;
 }
 
 type engine = caisar_env Caisar_reduction_engine.engine
@@ -41,9 +42,7 @@ let ls_of_caisar_op (env : engine) op =
   then Hashtbl.find_exn caisar_env.ls_of_caisar_op op
   else
     let id = Ident.id_fresh "caisar_op" in
-    let ty =
-      match op with Dataset _ -> caisar_env.dataset_ty | Size _ -> Ty.ty_int
-    in
+    let ty = match op with Dataset _ -> caisar_env.dataset_ty in
     let ls = Term.create_fsymbol id [] ty in
     Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
     Term.Hls.add caisar_env.caisar_op_of_ls ls op;
@@ -55,19 +54,24 @@ let caisar_op_of_ls env ls =
 
 let term_of_caisar_op env op = Term.t_app_infer (ls_of_caisar_op env op) []
 
-let read_caisar_env env =
+let read_caisar_env env cwd =
   let th = Env.read_theory env [ "caisar" ] "Interpret" in
   let dataset_ts = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
   {
     dataset_ty = Ty.ty_app dataset_ts [];
     ls_of_caisar_op = Hashtbl.Poly.create ();
     caisar_op_of_ls = Term.Hls.create 10;
+    cwd;
   }
 
 let print_caisar_op fmt caisar_env =
   Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
     fmt caisar_env.caisar_op_of_ls
 
+let compute_size_of_dataset ~cwd s =
+  let d = Caml.Filename.concat cwd s in
+  Array.length (Caml.Sys.readdir d)
+
 let built_in_caisar : caisar_env Caisar_reduction_engine.built_in_theories list
     =
   let open_dataset : _ Caisar_reduction_engine.builtin =
@@ -82,8 +86,9 @@ let built_in_caisar : caisar_env Caisar_reduction_engine.built_in_theories list
     match l with
     | [ Term { t_node = Tapp (ls, []); _ } ] -> (
       match caisar_op_of_ls engine ls with
-      | Dataset dataset -> Term (term_of_caisar_op engine (Size dataset))
-      | Size _ -> invalid_arg "We want a dataset! ;)")
+      | Dataset { dataset } ->
+        let cwd = (Caisar_reduction_engine.user_env engine).cwd in
+        Int (BigInt.of_int (compute_size_of_dataset ~cwd dataset)))
     | _ -> invalid_arg "We want a string! ;)"
   in
 
@@ -96,9 +101,9 @@ let built_in_caisar : caisar_env Caisar_reduction_engine.built_in_theories list
       [ ("open_dataset", None, open_dataset); ("size", None, size) ] );
   ]
 
-let interpret_task env task =
+let interpret_task ~cwd env task =
   let f = Task.task_goal_fmla task in
-  let caisar_env = read_caisar_env env in
+  let caisar_env = read_caisar_env env cwd in
   let engine =
     Caisar_reduction_engine.create
       {
@@ -115,12 +120,16 @@ let interpret_task env task =
   Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
     f print_caisar_op caisar_env
 
-let interpret ?debug ?format ~loadpath s =
+let interpret ?debug ?format ~loadpath (s : Verification.File.t) =
+  let cwd =
+    match s with Stdin -> Unix.getcwd () | File s -> Caml.Filename.dirname s
+    | JSON _ -> Unix.getcwd () (*todo *)
+  in
   let env, _config, mstr_theory =
     Verification.open_file ?debug ?format ~loadpath s
   in
   Wstdlib.Mstr.iter
     (fun _ theory ->
       List.iter (Task.split_theory theory None None) ~f:(fun task ->
-        interpret_task env task))
+        interpret_task ~cwd env task))
     mstr_theory

tests/dune

@@ -10,5 +10,7 @@
   bin/aimos
   bin/cvc5
   bin/nnenum.sh
-  filter_tmpdir.sh)
+  filter_tmpdir.sh
+  (glob_files "datasets/a/*")
+ )
  (package caisar))

tests/interpretation.t

@@ -21,15 +21,9 @@ Test verify
   
   G2 : false
   
-  Reduction engine, ident not found: infix =
-  G3 : caisar_op = 2
-  caisar_op1,
-  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+  G3 : true
   caisar_op,
-  (Interpretation.Size { Interpretation.dataset = "datasets/a" })
-  Reduction engine, ident not found: infix =
-  G4 : caisar_op2 = 2
-  caisar_op3,
   (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
-  caisar_op2,
-  (Interpretation.Size { Interpretation.dataset = "datasets/a" })
+  G4 : true
+  caisar_op1,
+  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })