src/HOL/Tools/Sledgehammer/sledgehammer_print.ML

adapted code for Z3 proof reconstruction

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_print.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Steffen Juilf Smolka, TU Muenchen

Basic mapping from proof data structures to proof strings.
*)

signature SLEDGEHAMMER_PRINT =
sig
  type isar_proof = Sledgehammer_Proof.isar_proof
  type reconstructor = Sledgehammer_Reconstructor.reconstructor
  type one_line_params = Sledgehammer_Reconstructor.one_line_params

  val string_of_reconstructor : reconstructor -> string

  val one_line_proof_text : int -> one_line_params -> string

  val string_of_proof :
    Proof.context -> string -> string -> int -> int -> isar_proof -> string
end;

structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
struct

open ATP_Util
open ATP_Proof
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Annotate


(** reconstructors **)

fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
    metis_call type_enc lam_trans
  | string_of_reconstructor SMT = smtN



(** one-liner reconstructor proofs **)

fun show_time NONE = ""
  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"

(* FIXME: Various bugs, esp. with "unfolding"
fun unusing_chained_facts _ 0 = ""
  | unusing_chained_facts used_chaineds num_chained =
    if length used_chaineds = num_chained then ""
    else if null used_chaineds then "(* using no facts *) "
    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
*)

fun apply_on_subgoal _ 1 = "by "
  | apply_on_subgoal 1 _ = "apply "
  | apply_on_subgoal i n =
    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n

fun using_labels [] = ""
  | using_labels ls =
    "using " ^ space_implode " " (map string_of_label ls) ^ " "

fun command_call name [] =
    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"

fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
  (* unusing_chained_facts used_chaineds num_chained ^ *)
  using_labels ls ^ apply_on_subgoal i n ^
  command_call (string_of_reconstructor reconstr) ss

fun try_command_line banner time command =
  banner ^ ": " ^
  Active.sendback_markup [Markup.padding_command] command ^
  show_time time ^ "."

fun minimize_line _ [] = ""
  | minimize_line minimize_command ss =
    case minimize_command ss of
      "" => ""
    | command =>
      "\nTo minimize: " ^
      Active.sendback_markup [Markup.padding_command] command ^ "."

fun split_used_facts facts =
  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
        |> pairself (sort_distinct (string_ord o pairself fst))

fun one_line_proof_text num_chained
        (preplay, banner, used_facts, minimize_command, subgoal,
         subgoal_count) =
  let
    val (chained, extra) = split_used_facts used_facts
    val (failed, reconstr, ext_time) =
      case preplay of
        Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
      | Trust_Playable (reconstr, time) =>
        (false, reconstr,
         case time of
           NONE => NONE
         | SOME time =>
           if time = Time.zeroTime then NONE else SOME (true, time))
      | Failed_to_Play reconstr => (true, reconstr, NONE)
    val try_line =
      ([], map fst extra)
      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
                               num_chained
      |> (if failed then
            enclose "One-line proof reconstruction failed: "
                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
                     \solve this.)"
          else
            try_command_line banner ext_time)
  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end




(** detailed Isar proofs **)

val indent_size = 2

fun string_of_proof ctxt type_enc lam_trans i n proof =
  let
    val ctxt =
      (* make sure type constraint are actually printed *)
      ctxt |> Config.put show_markup false
      (* make sure only type constraints inserted by sh_annotate are printed *)
           |> Config.put Printer.show_type_emphasis false
           |> Config.put show_types false
           |> Config.put show_sorts false
           |> Config.put show_consts false

    val register_fixes = map Free #> fold Variable.auto_fixes

    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)

    fun of_indent ind = replicate_string (ind * indent_size) " "

    fun of_moreover ind = of_indent ind ^ "moreover\n"

    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "

    fun of_obtain qs nr =
      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
         "ultimately "
       else if nr = 1 orelse member (op =) qs Then then
         "then "
       else
         "") ^ "obtain"

    fun of_show_have qs = if member (op =) qs Show then "show" else "have"

    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"

    fun of_prove qs nr =
      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
        "ultimately " ^ of_show_have qs
      else if nr=1 orelse member (op =) qs Then then
        of_thus_hence qs
      else
        of_show_have qs

    fun add_term term (s, ctxt) =
      (s ^ (term
            |> singleton (Syntax.uncheck_terms ctxt)
            |> annotate_types ctxt
            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
            |> simplify_spaces
            |> maybe_quote),
       ctxt |> Variable.auto_fixes term)

    fun by_method method = "by " ^
      (case method of
        SimpM => "simp"
      | AutoM => "auto"
      | FastforceM => "fastforce"
      | ForceM => "force"
      | ArithM => "arith"
      | BlastM => "blast"
      | _ => raise Fail "Sledgehammer_Print: by_method")

    fun using_facts [] [] = ""
      | using_facts ls ss =
          "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "

    fun of_method ls ss MetisM =
          reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
      | of_method ls ss method =
          using_facts ls ss ^ by_method method

    fun of_byline ind options (ls, ss) method =
      let
        val ls = ls |> sort_distinct label_ord
        val ss = ss |> sort_distinct string_ord
      in
        "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss method
      end

    fun of_free (s, T) =
      maybe_quote s ^ " :: " ^
      maybe_quote (simplify_spaces (with_vanilla_print_mode
        (Syntax.string_of_typ ctxt) T))

    fun add_frees xs (s, ctxt) =
      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)

    fun add_fix _ [] = I
      | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
                        #> add_frees xs
                        #> add_suffix "\n"

    fun add_assm ind (l, t) =
      add_suffix (of_indent ind ^ "assume " ^ of_label l)
      #> add_term t
      #> add_suffix "\n"

    fun add_assms ind assms = fold (add_assm ind) assms

    fun add_step_post ind l t facts method options =
      add_suffix (of_label l)
      #> add_term t
      #> add_suffix (of_byline ind options facts method ^ "\n")

    fun of_subproof ind ctxt proof =
      let
        val ind = ind + 1
        val s = of_proof ind ctxt proof
        val prefix = "{ "
        val suffix = " }"
      in
        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
        String.extract (s, ind * indent_size,
                        SOME (size s - ind * indent_size - 1)) ^
        suffix ^ "\n"
      end

    and of_subproofs _ _ _ [] = ""
      | of_subproofs ind ctxt qs subproofs =
        (if member (op =) qs Then then of_moreover ind else "") ^
        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)

    and add_step_pre ind qs subproofs (s, ctxt) =
      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)

    and add_step ind (Let (t1, t2)) =
        add_suffix (of_indent ind ^ "let ")
        #> add_term t1
        #> add_suffix " = "
        #> add_term t2
        #> add_suffix "\n"
      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, method))) =
        (case xs of
          [] => (* have *)
            add_step_pre ind qs subproofs
            #> add_suffix (of_prove qs (length subproofs) ^ " ")
            #> add_step_post ind l t facts method ""
        | _ => (* obtain *)
            add_step_pre ind qs subproofs
            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
            #> add_frees xs
            #> add_suffix " where "
            (* The new skolemizer puts the arguments in the same order as the
               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
               regarding Vampire). *)
            #> add_step_post ind l t facts method
                 (if exists (fn (_, T) => length (binder_types T) > 1) xs
                  andalso method = MetisM then
                    "using [[metis_new_skolem]] "
                  else
                    ""))

    and add_steps ind = fold (add_step ind)

    and of_proof ind ctxt (Proof (xs, assms, steps)) =
      ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
  in
    (* One-step Metis proofs are pointless; better use the one-liner directly. *)
    (case proof of
      Proof ([], [], [Prove (_, [], _, _, [], (_, MetisM))]) => ""
    | _ =>
      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
      of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
      of_indent 0 ^ (if n <> 1 then "next" else "qed"))
  end

end;