log.ml

(* ========================================================================= *)
(* Tactic logging machinery (for machine learning use)                       *)
(*                                                                           *)
(*                  (c) Copyright, Google Inc. 2017                          *)
(* ========================================================================= *)

set_jrh_lexer;;
Pb_printer.set_file_tags ["log.ml"];;
open List;;
open Fusion;;
open Printer;;
open Pb_printer;;
open Equal;;
open Drule;;

type goal = (string * thm) list * term;;

type justification = instantiation -> (thm * thm proof_log) list -> thm * thm proof_log

and goalstate = (term list * instantiation) * goal list * justification

and tactic = goal -> goalstate

and thm_tactic = thm -> tactic

(* 'a = thm at first, then src after finalization *)
and 'a tactic_log =
  (* Goes away in final proof logs *)
  | Fake_log
  (* tactic *)
  | Abs_tac_log
  | Mk_comb_tac_log
  | Disch_tac_log
  | Eq_tac_log
  | Conj_tac_log
  | Disj1_tac_log
  | Disj2_tac_log
  | Refl_tac_log
  | Itaut_tac_log
  | Cheat_tac_log
  | Ants_tac_log
  | Raw_pop_all_tac_log
  | Raw_pop_tac_log of int * 'a  (* popped thm at int location is only logged, so this is not a thm_tactic *)
  (* thm_tactic *)
  | Label_tac_log of string * 'a
  | Accept_tac_log of 'a
  | Mp_tac_log of 'a
  | Disj_cases_tac_log of 'a
  | Contr_tac_log of 'a
  | Match_accept_tac_log of 'a
  | Match_mp_tac_log of 'a
  | Freeze_then_log of 'a
  | Backchain_tac_log of 'a
  | Imp_subst_tac_log of 'a
  | Raw_conjuncts_tac_log of 'a
  (* term -> tactic *)
  | Undisch_tac_log of term
  | Undisch_el_tac_log of term  (* flyspeck specific - see tactics_jordan.ml *)
  | X_gen_tac_log of term
  | Exists_tac_log of term
  | X_meta_exists_tac_log of term
  | Raw_subgoal_tac_log of term
  (* other *)
  | Conv_tac_log of string (* conv *)
  | Gen_rewrite_tac_log of string (* conv *) * 'a list
  | Spec_tac_log of term * term
  | X_choose_tac_log of term * 'a
  | Unify_accept_tac_log of term list * 'a
  | Trans_tac_log of 'a * term
  | Asm_meson_tac_log of 'a list
  | Asm_metis_tac_log of 'a list
  | Rewrite_tac_log of rewrite_type * 'a list
  | Simp_tac_log of 'a list
  | Subst1_tac_log of 'a
  | Real_arith_tac_log
  | Real_arith_tac2_log
  | Arith_tac_log

and rewrite_type =
  | Pure_rewrite_type
  | Rewrite_type
  | Pure_once_rewrite_type
  | Once_rewrite_type

and 'a proof_log = Proof_log of goal * 'a tactic_log * 'a proof_log list;;

type src =
  | Premise_src of thm  (* A theorem that existed before this proof *)
  | Hypot_src of int * int * thm (* (n,k,th) is the kth hypothesis, n steps from the tree root, with value th *)
  | Conj_left_src of src  (* x in `x /\ y` *)
  | Conj_right_src of src  (* y in `x /\ y` *)
  | Assume_src of term  (* Generated by ASSUME tm *)
  | Unknown_src of thm

(* ------------------------------------------------------------------------- *)
(* Replace the logging part of a tactic *)
(* ------------------------------------------------------------------------- *)

let conversion_registry : (string, conv) Hashtbl.t = Hashtbl.create 1000;;
let conv2conv_registry :
      (string, conv -> conv) Hashtbl.t = Hashtbl.create 1000;;

let replace_o str =
  String.init (String.length str)
              (fun i ->
                let chr = String.get str i in
                if chr == 'o' then 'O'
                else chr)

let replace_comb str =
  let tmp = Str.global_replace (Str.regexp "funpow") "FUNPOW" str in
  replace_o tmp

let get_tag_base description str = match Str.split (Str.regexp "[:]") str with
  | [] -> failwith ("Empty lookup tag for " ^ description)
  | h :: [] -> h
  | h :: t -> String.concat ":" t

let lookup_from_registry registry description tag =
  if Hashtbl.mem registry tag then (
    let conv = Hashtbl.find registry tag in
    Printf.printf "Retrieved %s '%s'\n" description tag;
    (if String.uppercase_ascii tag = replace_comb tag then
       (Printf.printf "Returning retrieved %s: %s\n" description tag;
        conv)
     else failwith (description ^ " is not replayable " ^ tag)))
  else failwith (description ^ " is not found: " ^ tag)

let register_entity registry description tag conv =
  let tag_base = get_tag_base description tag in
  let tag = tag_base in
  if Hashtbl.mem registry tag then (
    (* let rconv = Hashtbl.find registry tag in *)
    (if String.uppercase_ascii tag = replace_comb tag then
       conv (*Alternatively: rconv here to check failures immediately*)
     else
       conv))
  else (
    Hashtbl.replace registry tag conv;
    conv);;

let register_conv = register_entity conversion_registry "conversion";;
let register_conv2conv = register_entity conv2conv_registry "conv2conv";;
let lookup_conv = lookup_from_registry conversion_registry "conversion";;
let lookup_conv2conv =
  lookup_from_registry conv2conv_registry "conv2conv";;

let replace_tactic_log : thm tactic_log -> tactic -> tactic =
  fun log tac g ->
    let mvs, gl, just = tac g in
    mvs, gl, fun i l -> fst (just i l), Proof_log (g,log,map snd l)

let add_tactic_log' : goal -> thm tactic_log -> tactic -> tactic =
  fun g' log tac g ->
    let mvs, gl, just = tac g in
    mvs, gl, fun i l ->
      let th,log' = just i l in
      th, Proof_log (g', log, [log'])

let add_tactic_log : thm tactic_log -> tactic -> tactic =
  fun log tac g -> add_tactic_log' g log tac g

(* ------------------------------------------------------------------------- *)
(* Machinery defined later, but needed in tactics.ml                         *)
(* ------------------------------------------------------------------------- *)

let replay_proof_log_ref : (src proof_log -> tactic) option ref = ref None
let finalize_proof_log_ref : (int -> thm proof_log -> src proof_log) option ref = ref None

let replay_proof_log log = match !replay_proof_log_ref with
    Some f -> f log
  | None -> failwith "replay_proof_log_ref unset"

let finalize_proof_log before_thms log = match !finalize_proof_log_ref with
    Some f -> f before_thms log
  | None -> failwith "finalize_proof_log_ref unset"

(* ------------------------------------------------------------------------- *)
(* Parseable S-Expression printer for goals.                                 *)
(* ------------------------------------------------------------------------- *)

let sexp_goal (gl:goal) =
  let asl,w = gl in
  (* TODO(geoffreyi): Should we ignore the string tag on hypotheses? *)
  Snode [Sleaf "g"; Snode (map (fun (_,th) -> sexp_thm th) asl); sexp_term w]

(* ------------------------------------------------------------------------- *)
(* Parseable S-Expression printer for goals. Ignoring the tag and            *)
(* hypotheses.                                                               *)
(* ------------------------------------------------------------------------- *)
let sexp_goal_stripped (gl:goal) =
  let asl,w = gl in
  Snode [Sleaf "g"; Snode (map (fun (_,th) -> sexp_term (concl th)) asl);
         sexp_term w]

(* ------------------------------------------------------------------------- *)
(* Parseable S-Expression printer for proof logs.                            *)
(* ------------------------------------------------------------------------- *)


(* TODO(smloos) implement this function.
   Will need to build data structure throughout _CONV tactics. *)
let sexp_conv conv = Sleaf "Conv_printing_not_implemented";;

(* TODO(smloos) implement this function. *)
let sexp_thm_tactic th_tac = Sleaf "thm_tactic_printing_not_implemented";;

(* Statistics *)
type proof_stats = {
  tactics : (string, int) Hashtbl.t;
  mutable total_tactics : int;
  (* Each proof has tactic_count, premises *)
  mutable proof_info : (int * int) list;
}
let empty_stats () = { tactics = Hashtbl.create 40;
                       total_tactics = 0;
                       proof_info = [] }
let all_stats = empty_stats ()
let replay_stats = empty_stats ()

let print_statistics name st =
  Printf.printf "\n***** %s *****\n" name;
  List.iter (fun (name,count) -> Printf.printf "%s: %d\n" name count)
    (List.sort compare (Hashtbl.fold (fun k v l -> (k,v)::l) st.tactics []));
  let proofs = length st.proof_info in
  Printf.printf "\ntotal proofs: %d\n" proofs;
  Printf.printf "total tactics: %d\n" st.total_tactics;
  if proofs != 0 then
    let stats name counts =
      let mean = float_of_int (fold_left (+) 0 counts) /. float_of_int proofs in
      let dev = sqrt (fold_left (+.) 0. (map (fun x ->
          let s = float_of_int x -. mean in s *. s) counts) /.
          float_of_int proofs) in
      Printf.printf "%s:\n  mean %g +- %g\n  quantiles:" name mean dev;
      let sorted = List.sort compare counts in
      let quantile q = List.nth sorted (min (proofs - 1) (proofs * q / 100)) in
      List.iter (fun q -> Printf.printf " %d%%:%d" q (quantile q))
                [0;10;20;30;40;50;60;70;80;90;100];
      Printf.printf "\n" in
    stats "tactics per proof" (map (fun (t,_) -> t) st.proof_info);
    stats "premises per proof" (map (fun (_,t) -> t) st.proof_info);
    Printf.printf "total thm objects: %d\n" (thm_count ())

let tactic_name_short taclog =
  match taclog with
    Fake_log -> "Fake"
  | Label_tac_log _ -> "Label_tac"
  | Accept_tac_log _ -> "Accept_tac"
  | Conv_tac_log _ -> "Conv_tac"
  | Abs_tac_log -> "Abs_tac"
  | Mk_comb_tac_log -> "Mk_comb_tac"
  | Disch_tac_log -> "Disch_tac"
  | Mp_tac_log _ -> "Mp_tac"
  | Eq_tac_log -> "Eq_tac"
  | Undisch_tac_log _ -> "Undisch_tac"
  | Undisch_el_tac_log _ -> "Undisch_el_tac"
  | Spec_tac_log _ -> "Spec_tac"
  | X_gen_tac_log _ -> "X_gen_tac"
  | X_choose_tac_log _ -> "X_choose_tac"
  | Exists_tac_log _ -> "Exists_tac"
  | Conj_tac_log -> "Conj_tac"
  | Disj1_tac_log -> "Disj1_tac"
  | Disj2_tac_log -> "Disj2_tac"
  | Disj_cases_tac_log _ -> "Disj_cases_tac"
  | Contr_tac_log _ -> "Contr_tac"
  | Match_accept_tac_log _ -> "Match_accept_tac"
  | Match_mp_tac_log _ -> "Match_mp_tac"
  | Raw_conjuncts_tac_log _ -> "Raw_conjuncts_tac"
  | Raw_subgoal_tac_log _ -> "Raw_subgoal_tac"
  | Freeze_then_log _ -> "Freeze_then"
  | X_meta_exists_tac_log _ -> "X_mpeta_exists_tac"
  | Backchain_tac_log _ -> "Backchain_tac"
  | Imp_subst_tac_log _ -> "Imp_subst_tac"
  | Unify_accept_tac_log _ -> "Unify_accept_tac"
  | Refl_tac_log -> "Refl_tac"
  | Trans_tac_log _ -> "Trans_tac"
  | Itaut_tac_log -> "Itaut_tac"
  | Cheat_tac_log -> "Cheat_tac"
  | Ants_tac_log -> "Ants_tac"
  | Raw_pop_tac_log _ -> "Raw_pop_tac"
  | Raw_pop_all_tac_log -> "Raw_pop_all_tac"
  | Asm_meson_tac_log _ -> "Asm_meson_tac"
  | Asm_metis_tac_log _ -> "Asm_metis_tac"
  | Simp_tac_log _ -> "Simp_tac"
  | Subst1_tac_log _ -> "Subst1_tac"
  | Real_arith_tac_log -> "Real_arith_tac"
  | Real_arith_tac2_log -> "Real_arith_tac2"
  | Arith_tac_log -> "Arith_tac"
  | Gen_rewrite_tac_log _ -> "Gen_rewrite_tac"
  | Rewrite_tac_log (ty,_) -> match ty with
      Pure_rewrite_type -> "Pure_rewrite_tac"
    | Rewrite_type -> "Rewrite_tac"
    | Pure_once_rewrite_type -> "Pure_once_rewrite_tac"
    | Once_rewrite_type -> "Once_rewrite_tac"

let tactic_name taclog = tactic_name_short taclog ^ "_log"

let tactic_sep_name taclog =
  ";" ^ (tactic_name taclog) ^ ";"

let rec sexp_src src = match src with
  | Premise_src th -> Snode [Sleaf "Premise_src"; sexp_thm th]
  | Hypot_src (n,k,th) -> Snode [Sleaf "Hypot_src";
                                 Sleaf (string_of_int n);
                                 Sleaf (string_of_int k);
                                 sexp_thm th]
  | Conj_left_src s -> Snode [Sleaf "Conj_left_src"; sexp_src s]
  | Conj_right_src s -> Snode [Sleaf "Conj_right_src"; sexp_src s]
  | Assume_src tm -> Snode [Sleaf "Assume_src"; sexp_term tm]
  | Unknown_src _ -> Snode [Sleaf "Unknown_src"]

let rec sexp_loc_src src = match src with
  | Premise_src th -> Snode [sexp_thm th; Sleaf " Premise_src <thm_end> "]
  | Hypot_src (n,k,th) -> Snode [sexp_thm th; Sleaf " Hypot_src <thm_end> "]
  | Conj_left_src s -> sexp_src s
  | Conj_right_src s -> sexp_src s
  | Assume_src tm -> Snode [sexp_term tm; Sleaf " Assume_src <thm_end> "]
  | Unknown_src _ -> Snode [Sleaf " Unknown_src <thm_end> "]

let sexp_tactic_log f taclog =
  let name = Sleaf (tactic_name taclog) in
  match taclog with
    (* tactic *)
      Fake_log
    | Abs_tac_log
    | Mk_comb_tac_log
    | Disch_tac_log
    | Eq_tac_log
    | Conj_tac_log
    | Disj1_tac_log
    | Disj2_tac_log
    | Refl_tac_log
    | Itaut_tac_log
    | Cheat_tac_log
    | Raw_pop_all_tac_log
    | Real_arith_tac_log
    | Real_arith_tac2_log
    | Arith_tac_log
    | Ants_tac_log -> Snode [name]
    (* thm_tactic *)
    | Accept_tac_log th
    | Mp_tac_log th
    | Disj_cases_tac_log th
    | Contr_tac_log th
    | Match_accept_tac_log th
    | Match_mp_tac_log th
    | Backchain_tac_log th
    | Subst1_tac_log th
    | Raw_conjuncts_tac_log th
    | Imp_subst_tac_log th -> Snode [name; f th]
    (* term -> tactic *)
    | Undisch_tac_log tm
    | Undisch_el_tac_log tm
    | X_gen_tac_log tm
    | Exists_tac_log tm
    | Raw_subgoal_tac_log tm
    | X_meta_exists_tac_log tm -> Snode [name; sexp_term tm]
    (* other *)
    | Label_tac_log (st, th) -> Snode [name; Sleaf st; f th]
    | Conv_tac_log c -> Snode [name; sexp_conv c]
    | Spec_tac_log (tm1, tm2) -> Snode [name; sexp_term tm1; sexp_term tm2]
    | X_choose_tac_log (tm, th) -> Snode [name; sexp_term tm; f th]
    | Freeze_then_log th -> Snode [name; f th]
    | Unify_accept_tac_log (tml, th) -> Snode [name; Snode (map sexp_term tml); f th]
    | Trans_tac_log (th,tm) -> Snode [name; f th; sexp_term tm]
    | Raw_pop_tac_log (n,th) -> Snode [name; Sleaf (string_of_int n); f th]
    | Asm_meson_tac_log thl
    | Asm_metis_tac_log thl
    | Simp_tac_log thl
    | Rewrite_tac_log (_,thl) -> Snode [name; Snode (map f thl)]
    | Gen_rewrite_tac_log (convs,thl) -> Snode [name; Sleaf convs; Snode (map f thl)]

let rec sexp_proof_log f (Proof_log (gl, taclog, logl)) =
  Snode [Sleaf "p"; sexp_goal gl; sexp_tactic_log f taclog; Snode (map (sexp_proof_log f) logl)]

let rec sexp_proof_log_flatten_stripped f (Proof_log (gl, taclog, logl)) =
  Snode [Sleaf "p"; sexp_goal_stripped gl; Sleaf (tactic_name taclog)] ::
    List.concat (map (sexp_proof_log_flatten_stripped f) logl)

(* Create an s-expr of tactics applied in a proof log. *)
let rec sexp_tac_names log =
  let rec sexp_tac_names_ls (Proof_log (gl, taclog, logl)) =
    (Sleaf (tactic_name taclog))::
      (match logl with
         [] -> []
       | hd::[] -> sexp_tac_names_ls hd
       | _ -> map sexp_tac_names logl) in
  Snode (sexp_tac_names_ls log)

(* Create an s-expr with goal-terms followed by the tactic applied to it. *)
let rec sexp_term_tac_names log =
  let rec sexp_term_tac_names_ls (Proof_log ((ths, tm), taclog, logl)) =
    sexp_term tm::
      ((Sleaf (tactic_name taclog))::
         (match logl with
            [] -> []
          | hd::[] -> sexp_term_tac_names_ls hd
          | _ -> map sexp_term_tac_names logl)) in
  Snode (sexp_term_tac_names_ls log)

let sleaf s = (Sleaf s)

(* Create an s-expr with goalstate (asl,w), tactic name, and parameters. *)
let rec sexp_flat_tac_params f (Proof_log ((ths, tm), taclog, logl)) =
  sexp_term tm :: (Sleaf " <goalterm>; ") ::
    (Snode (map sleaf (map fst ths))) :: (Sleaf " <goalthmstr>; ") ::
      (Snode (map sexp_thm (map snd ths))) :: (Sleaf " <goalthms>; ") ::
        (Sleaf (tactic_name taclog)) :: (Sleaf " <tactic>; ") ::
          (sexp_tactic_log sexp_loc_src taclog) :: (Sleaf " <parameterls>; ") ::
            (Sleaf " <end>; ") :: List.concat (map (sexp_flat_tac_params f) logl)

(* Create a list of s-exprs alternating goal-term and tactic *)
let rec sexp_flat_tac (Proof_log ((ths, tm), taclog, logl)) =
  sexp_term tm :: (Sleaf (tactic_sep_name taclog) ::
                     List.concat (map sexp_flat_tac logl))

let referenced_thms plog =
  let seen : (int, unit) Hashtbl.t = Hashtbl.create 1 in
  let rec visit src = match src with
      Premise_src th -> Hashtbl.replace seen (thm_id th) ()
    | Conj_left_src s -> visit s
    | Conj_right_src s -> visit s
    | Hypot_src _ | Assume_src _ | Unknown_src _ -> () in
  let rec visit_plog (Proof_log (_,tac,logs)) =
    visit_tac tac;
    List.iter visit_plog logs
  and visit_tac tac = match tac with
    (* 0 thms *)
    | Fake_log
    | Conv_tac_log _
    | Abs_tac_log
    | Mk_comb_tac_log
    | Disch_tac_log
    | Eq_tac_log
    | Undisch_tac_log _
    | Undisch_el_tac_log _
    | Spec_tac_log _
    | X_gen_tac_log _
    | Exists_tac_log _
    | Conj_tac_log
    | Disj1_tac_log
    | Disj2_tac_log
    | Raw_subgoal_tac_log _
    | X_meta_exists_tac_log _
    | Refl_tac_log
    | Itaut_tac_log
    | Cheat_tac_log
    | Ants_tac_log
    | Arith_tac_log
    | Real_arith_tac_log
    | Real_arith_tac2_log
    | Raw_pop_all_tac_log -> ()
    (* 1 thm *)
    | Raw_pop_tac_log (_,th)
    | Label_tac_log (_,th)
    | Accept_tac_log th
    | Mp_tac_log th
    | X_choose_tac_log (_,th)
    | Disj_cases_tac_log th
    | Contr_tac_log th
    | Match_accept_tac_log th
    | Match_mp_tac_log th
    | Raw_conjuncts_tac_log th
    | Freeze_then_log th
    | Backchain_tac_log th
    | Imp_subst_tac_log th
    | Unify_accept_tac_log (_,th)
    | Subst1_tac_log th
    | Trans_tac_log (th,_) -> visit th
    (* thm list *)
    | Asm_meson_tac_log thl
    | Asm_metis_tac_log thl
    | Simp_tac_log thl
    | Gen_rewrite_tac_log (_,thl)
    | Rewrite_tac_log (_,thl) -> List.iter visit thl

  in
    visit_plog plog;
    Hashtbl.fold (fun i () l -> i :: l) seen []

let add_proof_stats st plog =
    let rec loop (Proof_log (gl, taclog, logl)) =
      let name = tactic_name taclog in
      let count = try Hashtbl.find st.tactics name with Not_found -> 0 in
      Hashtbl.replace st.tactics name (succ count);
      st.total_tactics <- succ st.total_tactics;
      List.iter loop logl in
  let before_tactics = st.total_tactics in
  loop plog;
  let after_tactics = st.total_tactics in
  let thl = referenced_thms plog in
  st.proof_info <- (after_tactics - before_tactics, length thl) :: st.proof_info


(* ---------------------------------------------------------------------------*)
(* Creates a map from subgoals to theorems to file specified in environment   *)
(* variable SUBGOAL_DEPENDENCIES_LOG_OUTPUT.                                  *)
(* ---------------------------------------------------------------------------*)

let rec collect_subgoals (Proof_log (g,_,logs) : 'a proof_log) : goal list =
  g :: concat (map collect_subgoals logs)

let sexp_subgoal_dependendies (Proof_log (g,_,logs) : 'a proof_log) : sexp =
  Snode (sexp_goal g ::
         Sleaf "->" ::
         map sexp_goal (concat (map collect_subgoals logs)));;


(* ---------------------------------------------------------------------------*)
(* Common code for logging hooks                                              *)
(* ---------------------------------------------------------------------------*)

let try_to_print (f : 'a proof_log -> Format.formatter -> unit)
                 (log : 'a proof_log)
                 (fmt_o : Format.formatter option) : unit =
  match fmt_o with
    Some fmt ->
      f log fmt;
      Format.pp_print_flush fmt ();
  | None -> ();;


(* ---------------------------------------------------------------------------*)
(* Prooflog protobuf printing                                                 *)
(* ---------------------------------------------------------------------------*)

let rec extract_thm (asm_thm: src) : thm = match asm_thm with
    Hypot_src (_, _, thm)
  | Premise_src thm
  | Unknown_src thm -> thm
  | Assume_src term -> ASSUME term
  | Conj_left_src asm_thm
  | Conj_right_src asm_thm -> extract_thm asm_thm

let tactic_argument_term fmt (t: term) : unit =
  pp_print_string fmt " parameters {";
  pp_print_string fmt " parameter_type: TERM";
  pp_print_string fmt " term: \"";
  sexp_print fmt (sexp_term (Normalize.normalize_term t));
  pp_print_string fmt  "\"";
  pp_print_string fmt "}";;

let tactic_argument_string
    fmt pb_type pb_field
    (print_item: 'a -> unit)
    (items: 'a list) : unit =
  pp_print_string fmt " parameters {";
  pp_print_string fmt (" parameter_type: " ^ pb_type);
  List.iter
      (fun item ->
        pp_print_string fmt (" " ^ pb_field ^ ": \"");
        print_item item;
        pp_print_string fmt "\"";)
      items;
  pp_print_string fmt "}";;

let tactic_argument_thms
    fmt
    (ptype: string)
    (print_item: thm -> unit)
    (items: thm list) : unit =
  pp_print_string fmt " parameters {";
  pp_print_string fmt (" parameter_type: " ^ ptype);
  List.iter
      (fun item ->
        pp_print_string fmt " theorems {";
        print_item item;
        pp_print_string fmt "}";)
      items;
  pp_print_string fmt "}";;

let tactic_argument_thm fmt ptype (srcs: src list) : unit =
  tactic_argument_thms
      fmt ptype
      (fun th ->
          print_thm_pb fmt (Normalize.normalize_theorem th) "THEOREM" (fun _ -> ()))
      (map extract_thm srcs);;

let tactic_arguments_pb fmt (taclog : src tactic_log) =
  match taclog with
  (* tactic *)
    Fake_log
  | Abs_tac_log
  | Mk_comb_tac_log
  | Disch_tac_log
  | Eq_tac_log
  | Conj_tac_log
  | Disj1_tac_log
  | Disj2_tac_log
  | Refl_tac_log
  | Itaut_tac_log
  | Cheat_tac_log
  | Raw_pop_all_tac_log
  | Real_arith_tac_log
  | Real_arith_tac2_log
  | Arith_tac_log
  | Ants_tac_log -> ()  (* No arguments to print *)

  (* thm_tactic *)
  | Accept_tac_log thm
  | Mp_tac_log thm
  | Disj_cases_tac_log thm
  | Contr_tac_log thm
  | Match_accept_tac_log thm
  | Match_mp_tac_log thm
  | Backchain_tac_log thm
  | Subst1_tac_log thm
  | Raw_conjuncts_tac_log thm
  | Imp_subst_tac_log thm -> tactic_argument_thm fmt "THEOREM" [thm]

  (* term -> tactic *)
  | Undisch_tac_log term
  | Undisch_el_tac_log term
  | X_gen_tac_log term
  | Exists_tac_log term
  | Raw_subgoal_tac_log term
  | X_meta_exists_tac_log term -> tactic_argument_term fmt term

  (* theorem list *)
  | Asm_meson_tac_log thms
  | Asm_metis_tac_log thms
  | Simp_tac_log thms
  | Rewrite_tac_log (_,thms) -> tactic_argument_thm fmt "THEOREM_LIST" thms

  (* other *)
  | Label_tac_log (st, thm) ->
      tactic_argument_string
          fmt "UNKNOWN" "unknown"
          (pp_print_string fmt)
          [st];
      tactic_argument_thm fmt "THEOREM" [thm]
  | Conv_tac_log conv ->
      tactic_argument_string fmt "CONV" "conv" (pp_print_string fmt) [conv];
  | Spec_tac_log (term1, term2) ->
      tactic_argument_term fmt term1;
      tactic_argument_term fmt term2
  | X_choose_tac_log (term, thm) ->
      tactic_argument_term fmt term;
      tactic_argument_thm fmt "THEOREM" [thm]
  | Freeze_then_log th -> ()  (* Not supported by deephol *)
  | Unify_accept_tac_log (terms, th) -> ()  (* Not supported by deephol *)
  | Trans_tac_log (thm, term) ->
      tactic_argument_thm fmt "THEOREM" [thm];
      tactic_argument_term fmt term
  | Raw_pop_tac_log (n, _) ->
      tactic_argument_string
          fmt "UNKNOWN" "unknown"
          (pp_print_string fmt)
          [string_of_int n];
  | Gen_rewrite_tac_log (conv, thms) ->
      tactic_argument_string fmt "CONV" "conv" (pp_print_string fmt) [conv];
      tactic_argument_thm fmt "THEOREM_LIST" thms;;


(* We assume the asl of goals contains only reflexive thms: A |- A.
   This function prints a comment when that assumption is violated. *)
let refl_thm_to_concl_temp (thms: thm list) : term list =
  let assert_refl (th: thm) : term =
    match dest_thm th with
      (hd::[], w) when hd == w -> w
    | (hd::[], w) -> (try ((ALPHA hd w);
                           Printf.printf "refl_thm_to_concl[ALPHA]: %s\n"
                                         (string_of_thm th))
                      with Failure _ ->
                        Printf.printf
                          "FAILURE refl_thm_to_concl[1] assumption != concl:\n %s\n"
                          (string_of_thm th));
                     w
    | (hd::tl, w) -> Printf.printf
                       "FAILURE refl_thm_to_concl[2] too many assumptions:\n %s\n"
                       (string_of_thm th);
                     w
    | (_, w) -> Printf.printf
                  "FAILURE refl_thm_to_concl[3] can't match assumptions:\n %s\n"
                  (string_of_thm th); w in
  map assert_refl thms

let goal_to_tuple (g: goal) : term list * term =
  (refl_thm_to_concl_temp (map snd (fst g)), snd g);;

let print_tactic_application_pb
    fmt
    (tl: src tactic_log)
    (subgoals: src proof_log list) =
  let tname: string = String.uppercase (tactic_name_short tl) in
  pp_print_string fmt (" proofs { tactic: \"" ^ tname ^ "\"");
  tactic_arguments_pb fmt tl;
  List.iter
    (fun (pl: 'a proof_log) ->
      match pl with Proof_log (subgoal, _, _) ->
        pp_print_string fmt " subgoals {";
        print_goal_pb fmt (goal_to_tuple subgoal) "GOAL" (fun _ -> ());
        pp_print_string fmt "}"
    ) subgoals;
  pp_print_string fmt " result: SUCCESS";
  pp_print_string fmt " closed: true";
  pp_print_string fmt "}";;

let rec print_prooflog_pb
    (theorem_in_database: thm)
    (tag: string)
    (log: src proof_log)
    (fmt: Format.formatter) : unit =
  match log with Proof_log (g, tl, subgoals) ->

    if String.equal tag "THEOREM" then
    (pp_print_string fmt "theorem_in_database {";
     print_thm_pb fmt theorem_in_database "THEOREM" (fun _ -> ());
     pp_print_string fmt  "}");

    pp_print_string fmt "nodes {";
    pp_print_string fmt " goal {";
    print_goal_pb fmt (goal_to_tuple g) "GOAL" (fun _ -> ());
    pp_print_string fmt "}";
    pp_print_string fmt " status: PROVED";
    print_tactic_application_pb fmt tl subgoals;
    pp_print_string fmt "}";

    (* prooflog nodes for subgoals *)
    List.iter
      (fun pl -> print_prooflog_pb theorem_in_database "GOAL" pl fmt)
      subgoals;

    if String.equal tag "THEOREM" then pp_print_string fmt "\n";;


(* ---------------------------------------------------------------------------*)
(* print_logs is the entry point for all proof logging.                       *)
(*                                                                            *)
(* This function also decides, for every proof (not proof step) whether it    *)
(* goes in test, valid, or train.                                             *)
(* ---------------------------------------------------------------------------*)
let log_proof (log : src proof_log) (th: thm) : unit =
  if List.length (hyp th) == 0 then
    try_to_print
        (print_prooflog_pb (Normalize.normalize_theorem th) "THEOREM")
        log
        prooflog_pb_fmt;;

let log_theorem (th: thm) (source: string) (goal_fingerprint: int option) =
  if List.length (hyp th) == 0 then
    thm_db_print_theorem th source goal_fingerprint;;

Pb_printer.clear_file_tags();;