src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54504 096f7d452164
child 54700 64177ce0a7bd
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
smolkas@52590
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_print.ML
smolkas@52555
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@52555
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52555
     4
smolkas@52555
     5
Basic mapping from proof data structures to proof strings.
smolkas@52555
     6
*)
smolkas@52555
     7
smolkas@52555
     8
signature SLEDGEHAMMER_PRINT =
smolkas@52555
     9
sig
smolkas@52555
    10
  type isar_proof = Sledgehammer_Proof.isar_proof
smolkas@52555
    11
  type reconstructor = Sledgehammer_Reconstructor.reconstructor
smolkas@52555
    12
  type one_line_params = Sledgehammer_Reconstructor.one_line_params
smolkas@52555
    13
smolkas@52555
    14
  val string_of_reconstructor : reconstructor -> string
smolkas@52555
    15
wenzelm@53052
    16
  val one_line_proof_text : int -> one_line_params -> string
smolkas@52555
    17
smolkas@52555
    18
  val string_of_proof :
smolkas@52555
    19
    Proof.context -> string -> string -> int -> int -> isar_proof -> string
smolkas@52555
    20
end;
smolkas@52555
    21
smolkas@52555
    22
structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
smolkas@52555
    23
struct
smolkas@52555
    24
smolkas@52555
    25
open ATP_Util
smolkas@52555
    26
open ATP_Proof
smolkas@52555
    27
open ATP_Problem_Generate
smolkas@52555
    28
open ATP_Proof_Reconstruct
smolkas@52555
    29
open Sledgehammer_Util
smolkas@52555
    30
open Sledgehammer_Reconstructor
smolkas@52555
    31
open Sledgehammer_Proof
smolkas@52555
    32
open Sledgehammer_Annotate
smolkas@52555
    33
smolkas@52555
    34
smolkas@52555
    35
(** reconstructors **)
smolkas@52555
    36
smolkas@52555
    37
fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
smolkas@52555
    38
    metis_call type_enc lam_trans
smolkas@52555
    39
  | string_of_reconstructor SMT = smtN
smolkas@52555
    40
smolkas@52555
    41
smolkas@52555
    42
smolkas@52555
    43
(** one-liner reconstructor proofs **)
smolkas@52555
    44
smolkas@52555
    45
fun show_time NONE = ""
smolkas@52555
    46
  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
smolkas@52555
    47
smolkas@52555
    48
(* FIXME: Various bugs, esp. with "unfolding"
smolkas@52555
    49
fun unusing_chained_facts _ 0 = ""
smolkas@52555
    50
  | unusing_chained_facts used_chaineds num_chained =
smolkas@52555
    51
    if length used_chaineds = num_chained then ""
smolkas@52555
    52
    else if null used_chaineds then "(* using no facts *) "
smolkas@52555
    53
    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
smolkas@52555
    54
*)
smolkas@52555
    55
smolkas@52555
    56
fun apply_on_subgoal _ 1 = "by "
smolkas@52555
    57
  | apply_on_subgoal 1 _ = "apply "
smolkas@52555
    58
  | apply_on_subgoal i n =
smolkas@52555
    59
    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
smolkas@52555
    60
smolkas@52555
    61
fun using_labels [] = ""
smolkas@52555
    62
  | using_labels ls =
smolkas@52555
    63
    "using " ^ space_implode " " (map string_of_label ls) ^ " "
smolkas@52555
    64
smolkas@52555
    65
fun command_call name [] =
smolkas@52555
    66
    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
smolkas@52555
    67
  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
smolkas@52555
    68
smolkas@52555
    69
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
smolkas@52555
    70
  (* unusing_chained_facts used_chaineds num_chained ^ *)
smolkas@52555
    71
  using_labels ls ^ apply_on_subgoal i n ^
smolkas@52555
    72
  command_call (string_of_reconstructor reconstr) ss
smolkas@52555
    73
wenzelm@53052
    74
fun try_command_line banner time command =
wenzelm@52697
    75
  banner ^ ": " ^
wenzelm@53052
    76
  Active.sendback_markup [Markup.padding_command] command ^
wenzelm@52697
    77
  show_time time ^ "."
smolkas@52555
    78
wenzelm@53052
    79
fun minimize_line _ [] = ""
wenzelm@53052
    80
  | minimize_line minimize_command ss =
smolkas@52555
    81
    case minimize_command ss of
smolkas@52555
    82
      "" => ""
smolkas@52555
    83
    | command =>
wenzelm@53052
    84
      "\nTo minimize: " ^
wenzelm@53052
    85
      Active.sendback_markup [Markup.padding_command] command ^ "."
smolkas@52555
    86
smolkas@52555
    87
fun split_used_facts facts =
smolkas@52555
    88
  facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
smolkas@52555
    89
        |> pairself (sort_distinct (string_ord o pairself fst))
smolkas@52555
    90
wenzelm@53052
    91
fun one_line_proof_text num_chained
smolkas@52555
    92
        (preplay, banner, used_facts, minimize_command, subgoal,
smolkas@52555
    93
         subgoal_count) =
smolkas@52555
    94
  let
smolkas@52555
    95
    val (chained, extra) = split_used_facts used_facts
smolkas@52555
    96
    val (failed, reconstr, ext_time) =
smolkas@52555
    97
      case preplay of
smolkas@52555
    98
        Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
smolkas@52555
    99
      | Trust_Playable (reconstr, time) =>
smolkas@52555
   100
        (false, reconstr,
smolkas@52555
   101
         case time of
smolkas@52555
   102
           NONE => NONE
smolkas@52555
   103
         | SOME time =>
smolkas@52555
   104
           if time = Time.zeroTime then NONE else SOME (true, time))
smolkas@52555
   105
      | Failed_to_Play reconstr => (true, reconstr, NONE)
smolkas@52555
   106
    val try_line =
smolkas@52555
   107
      ([], map fst extra)
smolkas@52555
   108
      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
smolkas@52555
   109
                               num_chained
smolkas@52555
   110
      |> (if failed then
smolkas@52555
   111
            enclose "One-line proof reconstruction failed: "
smolkas@52555
   112
                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
smolkas@52555
   113
                     \solve this.)"
smolkas@52555
   114
          else
wenzelm@53052
   115
            try_command_line banner ext_time)
wenzelm@53052
   116
  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
smolkas@52555
   117
smolkas@52555
   118
smolkas@52555
   119
smolkas@52555
   120
smolkas@52555
   121
(** detailed Isar proofs **)
smolkas@52555
   122
smolkas@52555
   123
val indent_size = 2
smolkas@52555
   124
smolkas@52555
   125
fun string_of_proof ctxt type_enc lam_trans i n proof =
smolkas@52555
   126
  let
smolkas@52555
   127
    val ctxt =
smolkas@52555
   128
      (* make sure type constraint are actually printed *)
smolkas@52555
   129
      ctxt |> Config.put show_markup false
smolkas@52555
   130
      (* make sure only type constraints inserted by sh_annotate are printed *)
smolkas@52555
   131
           |> Config.put Printer.show_type_emphasis false
smolkas@52555
   132
           |> Config.put show_types false
smolkas@52555
   133
           |> Config.put show_sorts false
smolkas@52555
   134
           |> Config.put show_consts false
smolkas@52592
   135
smolkas@52555
   136
    val register_fixes = map Free #> fold Variable.auto_fixes
smolkas@52592
   137
smolkas@52555
   138
    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
smolkas@52592
   139
smolkas@52555
   140
    fun of_indent ind = replicate_string (ind * indent_size) " "
smolkas@52592
   141
smolkas@52555
   142
    fun of_moreover ind = of_indent ind ^ "moreover\n"
smolkas@52592
   143
smolkas@52555
   144
    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
smolkas@52592
   145
smolkas@52555
   146
    fun of_obtain qs nr =
smolkas@52555
   147
      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
smolkas@52555
   148
         "ultimately "
blanchet@52994
   149
       else if nr = 1 orelse member (op =) qs Then then
smolkas@52555
   150
         "then "
smolkas@52555
   151
       else
smolkas@52555
   152
         "") ^ "obtain"
smolkas@52592
   153
smolkas@52555
   154
    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
smolkas@52592
   155
smolkas@52555
   156
    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
smolkas@52592
   157
smolkas@52555
   158
    fun of_prove qs nr =
smolkas@52555
   159
      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
smolkas@52555
   160
        "ultimately " ^ of_show_have qs
smolkas@52555
   161
      else if nr=1 orelse member (op =) qs Then then
smolkas@52555
   162
        of_thus_hence qs
smolkas@52555
   163
      else
smolkas@52555
   164
        of_show_have qs
smolkas@52592
   165
smolkas@52555
   166
    fun add_term term (s, ctxt) =
smolkas@52555
   167
      (s ^ (term
smolkas@52555
   168
            |> singleton (Syntax.uncheck_terms ctxt)
smolkas@52555
   169
            |> annotate_types ctxt
smolkas@52555
   170
            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
smolkas@52555
   171
            |> simplify_spaces
smolkas@52555
   172
            |> maybe_quote),
smolkas@52555
   173
       ctxt |> Variable.auto_fixes term)
smolkas@52592
   174
smolkas@52592
   175
    fun by_method method = "by " ^
smolkas@52592
   176
      (case method of
smolkas@52592
   177
        SimpM => "simp"
smolkas@52592
   178
      | AutoM => "auto"
smolkas@52592
   179
      | FastforceM => "fastforce"
smolkas@52629
   180
      | ForceM => "force"
smolkas@52592
   181
      | ArithM => "arith"
blanchet@53149
   182
      | BlastM => "blast"
smolkas@52592
   183
      | _ => raise Fail "Sledgehammer_Print: by_method")
smolkas@52592
   184
smolkas@52592
   185
    fun using_facts [] [] = ""
smolkas@52592
   186
      | using_facts ls ss =
smolkas@52592
   187
          "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
smolkas@52592
   188
smolkas@52592
   189
    fun of_method ls ss MetisM =
smolkas@52592
   190
          reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
smolkas@52592
   191
      | of_method ls ss method =
smolkas@52592
   192
          using_facts ls ss ^ by_method method
smolkas@52592
   193
smolkas@52592
   194
    fun of_byline ind options (ls, ss) method =
smolkas@52592
   195
      let
smolkas@52592
   196
        val ls = ls |> sort_distinct label_ord
smolkas@52592
   197
        val ss = ss |> sort_distinct string_ord
smolkas@52592
   198
      in
smolkas@52592
   199
        "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss method
smolkas@52592
   200
      end
smolkas@52592
   201
smolkas@52555
   202
    fun of_free (s, T) =
smolkas@52555
   203
      maybe_quote s ^ " :: " ^
smolkas@52555
   204
      maybe_quote (simplify_spaces (with_vanilla_print_mode
smolkas@52555
   205
        (Syntax.string_of_typ ctxt) T))
smolkas@52592
   206
smolkas@52555
   207
    fun add_frees xs (s, ctxt) =
smolkas@52555
   208
      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
smolkas@52592
   209
smolkas@52555
   210
    fun add_fix _ [] = I
smolkas@52555
   211
      | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
smolkas@52555
   212
                        #> add_frees xs
smolkas@52555
   213
                        #> add_suffix "\n"
smolkas@52592
   214
smolkas@52555
   215
    fun add_assm ind (l, t) =
smolkas@52555
   216
      add_suffix (of_indent ind ^ "assume " ^ of_label l)
smolkas@52555
   217
      #> add_term t
smolkas@52555
   218
      #> add_suffix "\n"
smolkas@52592
   219
smolkas@52555
   220
    fun add_assms ind assms = fold (add_assm ind) assms
smolkas@52592
   221
smolkas@52592
   222
    fun add_step_post ind l t facts method options =
smolkas@52555
   223
      add_suffix (of_label l)
smolkas@52555
   224
      #> add_term t
smolkas@52592
   225
      #> add_suffix (of_byline ind options facts method ^ "\n")
smolkas@52592
   226
smolkas@52555
   227
    fun of_subproof ind ctxt proof =
smolkas@52555
   228
      let
smolkas@52555
   229
        val ind = ind + 1
smolkas@52555
   230
        val s = of_proof ind ctxt proof
smolkas@52555
   231
        val prefix = "{ "
smolkas@52555
   232
        val suffix = " }"
smolkas@52555
   233
      in
smolkas@52555
   234
        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
smolkas@52555
   235
        String.extract (s, ind * indent_size,
smolkas@52555
   236
                        SOME (size s - ind * indent_size - 1)) ^
smolkas@52555
   237
        suffix ^ "\n"
smolkas@52555
   238
      end
smolkas@52592
   239
smolkas@52555
   240
    and of_subproofs _ _ _ [] = ""
smolkas@52555
   241
      | of_subproofs ind ctxt qs subproofs =
smolkas@52555
   242
        (if member (op =) qs Then then of_moreover ind else "") ^
smolkas@52555
   243
        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
smolkas@52592
   244
smolkas@52555
   245
    and add_step_pre ind qs subproofs (s, ctxt) =
smolkas@52555
   246
      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
smolkas@52592
   247
smolkas@52555
   248
    and add_step ind (Let (t1, t2)) =
smolkas@52555
   249
        add_suffix (of_indent ind ^ "let ")
smolkas@52555
   250
        #> add_term t1
smolkas@52555
   251
        #> add_suffix " = "
smolkas@52555
   252
        #> add_term t2
smolkas@52555
   253
        #> add_suffix "\n"
smolkas@52592
   254
      | add_step ind (Prove (qs, Fix xs, l, t, subproofs, By (facts, method))) =
smolkas@52555
   255
        (case xs of
smolkas@52555
   256
          [] => (* have *)
smolkas@52555
   257
            add_step_pre ind qs subproofs
smolkas@52555
   258
            #> add_suffix (of_prove qs (length subproofs) ^ " ")
smolkas@52592
   259
            #> add_step_post ind l t facts method ""
smolkas@52555
   260
        | _ => (* obtain *)
smolkas@52555
   261
            add_step_pre ind qs subproofs
smolkas@52555
   262
            #> add_suffix (of_obtain qs (length subproofs) ^ " ")
smolkas@52555
   263
            #> add_frees xs
smolkas@52555
   264
            #> add_suffix " where "
smolkas@52555
   265
            (* The new skolemizer puts the arguments in the same order as the
smolkas@52555
   266
               ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML"
smolkas@52555
   267
               regarding Vampire). *)
smolkas@52592
   268
            #> add_step_post ind l t facts method
smolkas@52592
   269
                 (if exists (fn (_, T) => length (binder_types T) > 1) xs
smolkas@52592
   270
                  andalso method = MetisM then
smolkas@52555
   271
                    "using [[metis_new_skolem]] "
smolkas@52555
   272
                  else
smolkas@52555
   273
                    ""))
smolkas@52592
   274
smolkas@52555
   275
    and add_steps ind = fold (add_step ind)
smolkas@52592
   276
smolkas@52555
   277
    and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
smolkas@52555
   278
      ("", ctxt)
smolkas@52555
   279
      |> add_fix ind xs
smolkas@52555
   280
      |> add_assms ind assms
smolkas@52555
   281
      |> add_steps ind steps
smolkas@52555
   282
      |> fst
smolkas@52592
   283
smolkas@52555
   284
  in
smolkas@52592
   285
    (* FIXME: sh_try0 might produce one-step proofs that are better than the
smolkas@52592
   286
       Metis one-liners *)
smolkas@52555
   287
    (* One-step proofs are pointless; better use the Metis one-liner
smolkas@52555
   288
       directly. *)
smolkas@52592
   289
    (*case proof of
smolkas@52555
   290
      Proof (Fix [], Assume [], [Prove (_, Fix [], _, _, [], _)]) => ""
smolkas@52592
   291
    | _ =>*) (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
smolkas@52555
   292
            of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
smolkas@52555
   293
            of_indent 0 ^ (if n <> 1 then "next" else "qed")
smolkas@52555
   294
  end
smolkas@52555
   295
blanchet@54504
   296
end;