[interpretation] Remove comments only useful for debugging.

src/interpretation.ml

@@ -67,8 +67,6 @@ type caisar_env = {
 
 let ls_of_caisar_op engine caisar_op ty_args ty =
   let caisar_env = CRE.user_env engine in
-  (* Fmt.pr "ls_of_caisar_op: %a@." pp_caisar_op op; *)
-  (* Option.iter ty ~f:(Fmt.pr "ty: %a@." Pretty.print_ty); *)
   Hashtbl.find_or_add caisar_env.ls_of_caisar_op caisar_op ~default:(fun () ->
     let id = Ident.id_fresh "caisar_op" in
     let ls =
@@ -77,7 +75,6 @@ let ls_of_caisar_op engine caisar_op ty_args ty =
       | Vector v -> v
       | _ -> Term.create_lsymbol id ty_args ty
     in
-    (* Fmt.pr "ls: %a@." Pretty.print_ls ls; *)
     Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:caisar_op ~data:ls;
     Term.Hls.add caisar_env.caisar_op_of_ls ls caisar_op;
     ls)
@@ -127,15 +124,11 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
   (* Vector *)
   let vget : _ CRE.builtin =
    fun engine ls vl ty ->
-    (* Fmt.pr "--@.vget: 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 = Tconst (ConstInt i); _ } as _t2);
     ] -> (
-      (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
       let i = Number.to_small_integer i in
       match caisar_op_of_ls engine ls1 with
       | Dataset (DS_csv csv) ->
@@ -160,16 +153,11 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         assert (List.length tl1 = n && i <= n);
         term (List.nth_exn tl1 i)
       | Data _ | NeuralNetwork _ -> 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 ])
+    | [ Term t1; Term t2 ] -> term (Term.t_app_infer ls [ t1; t2 ])
     | _ -> invalid_arg (error_message ls)
   in
   let length : _ CRE.builtin =
    fun engine ls vl _ty ->
-    (* Fmt.pr "--@.length: ls:%a , ty:%a@." Pretty.print_ls ls *)
-    (*   Fmt.(option ~none:nop Pretty.print_ty) *)
-    (*   ty; *)
     match vl with
     | [ Term { t_node = Tapp (ls, []); _ } ] -> (
       match caisar_op_of_ls engine ls with
@@ -185,22 +173,16 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         assert (List.length tl = n);
         int (BigInt.of_int n)
       | Dataset _ | Data _ | NeuralNetwork _ -> assert false)
-    | [ Term t ] ->
-      (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
-      term (Term.t_app_infer ls [ t ])
+    | [ Term t ] -> term (Term.t_app_infer ls [ t ])
     | _ -> invalid_arg (error_message ls)
   in
   let vminus : _ CRE.builtin =
    fun engine ls vl ty ->
-    (* Fmt.pr "--@.vminus: 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
       | Vector v, Data (D_csv data) ->
         let n = Option.value_exn (Language.lookup_vector v) in
@@ -228,23 +210,17 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         let caisar_op = Vector (Language.create_vector env n) in
         term (term_of_caisar_op ~args engine caisar_op ty)
       | _ -> 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 ])
+    | [ Term t1; Term t2 ] -> term (Term.t_app_infer ls [ t1; t2 ])
     | _ -> invalid_arg (error_message ls)
   in
   let mapi : _ CRE.builtin =
    fun engine ls vl ty ->
-    (* Fmt.pr "--@.mapi: 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 = Teps _tb; _ } as t2);
     ] -> (
       assert (Term.t_is_lambda t2);
-      (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
       match caisar_op_of_ls engine ls1 with
       | Vector v ->
         let n = Option.value_exn (Language.lookup_vector v) in
@@ -261,18 +237,13 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         Eval (term_of_caisar_op ~args engine caisar_op ty)
       | Dataset (DS_csv csv) -> int (BigInt.of_int (Csv.lines csv))
       | Data _ | NeuralNetwork _ -> 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 ])
+    | [ Term t1; Term t2 ] -> term (Term.t_app_infer ls [ t1; t2 ])
     | _ -> invalid_arg (error_message ls)
   in
 
   (* Neural Network *)
   let read_neural_network : _ CRE.builtin =
    fun engine ls vl ty ->
-    (* Fmt.pr "--@.read_neural_network: ls:%a , ty:%a@." Pretty.print_ls ls *)
-    (*   Fmt.(option ~none:nop Pretty.print_ty) *)
-    (*   ty; *)
     match vl with
     | [
      Term { t_node = Tconst (ConstStr neural_network); _ };
@@ -295,22 +266,14 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
   in
   let apply_neural_network : _ CRE.builtin =
    fun _engine ls vl _ty ->
-    (* Fmt.pr "--@.apply_neural_network: ls:%a , ty:%a@." Pretty.print_ls ls *)
-    (*   Fmt.(option ~none:nop Pretty.print_ty) *)
-    (*   ty; *)
     match vl with
-    | [ 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 ])
+    | [ Term t1; Term t2 ] -> term (Term.t_app_infer ls [ t1; t2 ])
     | _ -> invalid_arg (error_message ls)
   in
 
   (* Dataset *)
   let read_dataset : _ CRE.builtin =
    fun engine ls vl ty ->
-    (* Fmt.pr "--@.read_dataset: ls:%a , ty:%a@." Pretty.print_ls ls *)
-    (*   Fmt.(option ~none:nop Pretty.print_ty) *)
-    (*   ty; *)
     match vl with
     | [
      Term { t_node = Tconst (ConstStr dataset); _ };
@@ -357,8 +320,6 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
           ({ t_node = Tvar vs1; _ } as _t1);
           ({ t_node = Tconst (ConstInt n); _ } as _t2);
         ] ) ->
-    (* Fmt.pr "--@.has_length: %a %a@." Pretty.print_term t1 Pretty.print_term
-       t2; *)
     if not (Term.vs_equal vs vs1)
     then None
     else
@@ -414,7 +375,4 @@ let interpret_task ~cwd env task =
   let _, task = Task.task_separate_goal task in
   let task = declare_language_lsymbols caisar_env task in
   let task = Task.(add_prop_decl task Pgoal g f) in
-  (* Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task)
-     Pretty.print_term *)
-  (* f print_caisar_op_of_ls caisar_env; *)
   task