diff --git a/src/interpretation.ml b/src/interpretation.ml
index 791571a7c2bdf0f0309c88112217dcadbd1b24f8..e10ba5d615dfa5faeb6b2e8c3918c3e2b7228b38 100644
--- a/src/interpretation.ml
+++ b/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