[interpretation] Sleeping time.

src/interpretation.ml

@@ -42,6 +42,7 @@ type caisar_op =
 type caisar_env = {
   caisar_op_of_ls : caisar_op Term.Hls.t;
   ls_of_caisar_op : (caisar_op, Term.lsymbol) Hashtbl.t;
+  env : Env.env;
   cwd : string;
 }
 
@@ -65,10 +66,11 @@ let term_of_caisar_op ?(args = []) engine op ty =
   let t_args, ty_args = List.unzip args in
   Term.t_app_infer (ls_of_caisar_op engine op ty_args ty) t_args
 
-let caisar_env _env cwd =
+let caisar_env env cwd =
   {
     ls_of_caisar_op = Hashtbl.Poly.create ();
     caisar_op_of_ls = Term.Hls.create 10;
+    env;
     cwd;
   }
 
@@ -76,6 +78,20 @@ 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 const_real_of_float value =
+  let neg = Float.is_negative value in
+  let value = Fmt.str "%.64f" (Float.abs value) in
+  (* Split into integer and fractional parts. *)
+  let int_frac = String.split value ~on:'.' in
+  let int = List.hd_exn int_frac in
+  let frac =
+    match List.tl_exn int_frac with
+    | [] -> ""
+    | [ s ] -> s
+    | _ -> assert false (* Since every float has one '.' at most. *)
+  in
+  Constant.ConstReal (Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+
 let builtin_caisar : caisar_env CRE.built_in_theories list =
   let error_message ls =
     Fmt.str "Invalid arguments for '%a'" Pretty.print_ls ls
@@ -102,7 +118,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         in
         let ty_features =
           match ty with
-          | Some { ty_node = Tyapp (_, [ a; _ ]); _ } -> Some a
+          | Some { ty_node = Tyapp (_, [ ty; _ ]); _ } -> Some ty
           | _ -> assert false
         in
         let t_features, t_label =
@@ -134,19 +150,60 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
   (* Tensor *)
   let tget : _ CRE.builtin =
    fun engine ls vl ty ->
-    Fmt.pr "--@.hash_get: ls:%a , ty:%a@." Pretty.print_ls ls
+    Fmt.pr "--@.tget: ls:%a , ty:%a@." Pretty.print_ls ls
       Fmt.(option ~none:nop Pretty.print_ty)
       ty;
     match vl with
     | [
-     Term ({ t_node = Tapp (lsapp1, lsapp1_args); _ } as t1);
-     Term ({ t_node = Tapp (lsapp2, _); _ } as t2);
+     Term ({ t_node = Tapp (ls1, tl1); _ } as t1);
+     Term ({ t_node = Tapp (ls2, _); _ } as t2);
     ] -> (
       Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
-      match (caisar_op_of_ls engine lsapp1, caisar_op_of_ls engine lsapp2) with
-      | Tensor n1, Index (I_csv i1) ->
-        assert (i1 <= n1);
-        Term (List.nth_exn lsapp1_args i1)
+      match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
+      | Tensor n, Index (I_csv i) ->
+        assert (i <= n);
+        Term (List.nth_exn tl1 i)
+      | _ -> assert false)
+    | [ Term t1; Term t2 ] ->
+      Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+      Term (Term.t_app_infer ls [ t1; t2 ])
+    | _ -> invalid_arg (error_message ls)
+  in
+  let tminus : _ CRE.builtin =
+   fun engine ls vl ty ->
+    Fmt.pr "--@.tminus: ls:%a , ty:%a@." Pretty.print_ls ls
+      Fmt.(option ~none:nop Pretty.print_ty)
+      ty;
+    match vl with
+    | [
+     Term ({ t_node = Tapp (ls1, tl1); _ } as t1);
+     Term ({ t_node = Tapp (ls2, _); _ } as t2);
+    ] -> (
+      Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+      match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
+      | Tensor n, Data (D_csv d) ->
+        assert (n = List.length d);
+        let data_ty =
+          match ty with
+          | Some { ty_node = Tyapp (_, [ ty ]); _ } -> ty
+          | _ -> assert false
+        in
+        let data_cst =
+          List.map d ~f:(fun d ->
+            let cst = const_real_of_float (Float.of_string d) in
+            Term.t_const cst data_ty)
+        in
+        let minus =
+          (* TODO: generalize wrt [data_ty]. *)
+          let { env; _ } = CRE.user_env engine in
+          let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+          Theory.(ns_find_ls th.th_export [ Ident.op_infix ".-" ])
+        in
+        let args =
+          List.map2_exn tl1 data_cst ~f:(fun tl c ->
+            (Term.t_app_infer minus [ tl; c ], data_ty))
+        in
+        Term (term_of_caisar_op ~args engine (Tensor n) ty)
       | _ -> assert false)
     | [ Term t1; Term t2 ] ->
       Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
@@ -213,7 +270,11 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
       "Vector",
       [],
       [ (Ident.op_get "" (* ([]) *), None, vget); ("length", None, length) ] );
-    ([ "interpretation" ], "Tensor", [], [ (Ident.op_infix "#", None, tget) ]);
+    ( [ "interpretation" ],
+      "Tensor",
+      [],
+      [ (Ident.op_infix "#", None, tget); (Ident.op_infix "-", None, tminus) ]
+    );
     ( [ "interpretation" ],
       "Classifier",
       [],