src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57054 fed0329ea8e2
child 57287 68aa585269ac
permissions -rw-r--r--
simplified counterexample handling
blanchet@55287
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
smolkas@52555
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@52555
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@52555
     4
smolkas@52555
     5
Reconstructors.
smolkas@52555
     6
*)
smolkas@52555
     7
blanchet@55287
     8
signature SLEDGEHAMMER_PROOF_METHODS =
smolkas@52555
     9
sig
smolkas@52555
    10
  type stature = ATP_Problem_Generate.stature
smolkas@52555
    11
blanchet@55285
    12
  datatype proof_method =
blanchet@55285
    13
    Metis_Method of string option * string option |
blanchet@55285
    14
    Meson_Method |
blanchet@56081
    15
    SMT2_Method |
blanchet@56852
    16
    SATx_Method |
blanchet@55323
    17
    Blast_Method |
blanchet@55285
    18
    Simp_Method |
blanchet@55285
    19
    Simp_Size_Method |
blanchet@55285
    20
    Auto_Method |
blanchet@55285
    21
    Fastforce_Method |
blanchet@55285
    22
    Force_Method |
blanchet@55323
    23
    Linarith_Method |
blanchet@55323
    24
    Presburger_Method |
blanchet@55285
    25
    Algebra_Method
smolkas@52555
    26
blanchet@54824
    27
  datatype play_outcome =
blanchet@54824
    28
    Played of Time.time |
blanchet@54824
    29
    Play_Timed_Out of Time.time |
blanchet@56093
    30
    Play_Failed
smolkas@52555
    31
smolkas@52555
    32
  type minimize_command = string list -> string
blanchet@54824
    33
  type one_line_params =
blanchet@55285
    34
    (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
smolkas@52555
    35
blanchet@56985
    36
  val string_of_proof_method : Proof.context -> string list -> proof_method -> string
blanchet@57054
    37
  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
blanchet@55211
    38
  val string_of_play_outcome : play_outcome -> string
blanchet@55269
    39
  val play_outcome_ord : play_outcome * play_outcome -> order
blanchet@56985
    40
  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
blanchet@54495
    41
end;
smolkas@52555
    42
blanchet@55287
    43
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
smolkas@52555
    44
struct
smolkas@52555
    45
blanchet@54828
    46
open ATP_Util
smolkas@52555
    47
open ATP_Problem_Generate
blanchet@55211
    48
open ATP_Proof_Reconstruct
smolkas@52555
    49
blanchet@55285
    50
datatype proof_method =
blanchet@55285
    51
  Metis_Method of string option * string option |
blanchet@55285
    52
  Meson_Method |
blanchet@56081
    53
  SMT2_Method |
blanchet@56852
    54
  SATx_Method |
blanchet@55323
    55
  Blast_Method |
blanchet@55285
    56
  Simp_Method |
blanchet@55285
    57
  Simp_Size_Method |
blanchet@55285
    58
  Auto_Method |
blanchet@55285
    59
  Fastforce_Method |
blanchet@55285
    60
  Force_Method |
blanchet@55323
    61
  Linarith_Method |
blanchet@55323
    62
  Presburger_Method |
blanchet@55285
    63
  Algebra_Method
smolkas@52555
    64
blanchet@54824
    65
datatype play_outcome =
blanchet@54824
    66
  Played of Time.time |
blanchet@54824
    67
  Play_Timed_Out of Time.time |
blanchet@56093
    68
  Play_Failed
smolkas@52555
    69
blanchet@55211
    70
type minimize_command = string list -> string
blanchet@55211
    71
type one_line_params =
blanchet@55285
    72
  (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
blanchet@55211
    73
blanchet@56983
    74
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
blanchet@56983
    75
blanchet@56985
    76
fun string_of_proof_method ctxt ss meth =
blanchet@56983
    77
  let
blanchet@56983
    78
    val meth_s =
blanchet@56983
    79
      (case meth of
blanchet@56983
    80
        Metis_Method (NONE, NONE) => "metis"
blanchet@56983
    81
      | Metis_Method (type_enc_opt, lam_trans_opt) =>
blanchet@56983
    82
        "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
blanchet@56983
    83
      | Meson_Method => "meson"
blanchet@56983
    84
      | SMT2_Method => "smt2"
blanchet@56983
    85
      | SATx_Method => "satx"
blanchet@56983
    86
      | Blast_Method => "blast"
blanchet@56983
    87
      | Simp_Method => if null ss then "simp" else "simp add:"
blanchet@56985
    88
      | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
blanchet@56983
    89
      | Auto_Method => "auto"
blanchet@56983
    90
      | Fastforce_Method => "fastforce"
blanchet@56983
    91
      | Force_Method => "force"
blanchet@56983
    92
      | Linarith_Method => "linarith"
blanchet@56983
    93
      | Presburger_Method => "presburger"
blanchet@56983
    94
      | Algebra_Method => "algebra")
blanchet@56983
    95
  in
blanchet@56983
    96
    maybe_paren (space_implode " " (meth_s :: ss))
blanchet@56983
    97
  end
blanchet@55285
    98
blanchet@57054
    99
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
blanchet@56965
   100
  Method.insert_tac local_facts THEN'
blanchet@56965
   101
  (case meth of
blanchet@56965
   102
    Metis_Method (type_enc_opt, lam_trans_opt) =>
blanchet@56965
   103
    Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
blanchet@56965
   104
      (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
blanchet@56965
   105
  | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
blanchet@56965
   106
  | SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts
blanchet@56983
   107
  | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
blanchet@56965
   108
  | _ =>
blanchet@56965
   109
    Method.insert_tac global_facts THEN'
blanchet@55285
   110
    (case meth of
blanchet@56965
   111
      SATx_Method => SAT.satx_tac ctxt
blanchet@56965
   112
    | Blast_Method => blast_tac ctxt
blanchet@56965
   113
    | Simp_Size_Method =>
blanchet@56965
   114
      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
blanchet@56965
   115
    | Auto_Method => K (Clasimp.auto_tac ctxt)
blanchet@56965
   116
    | Fastforce_Method => Clasimp.fast_force_tac ctxt
blanchet@56965
   117
    | Force_Method => Clasimp.force_tac ctxt
blanchet@56965
   118
    | Linarith_Method => Lin_Arith.tac ctxt
blanchet@56965
   119
    | Presburger_Method => Cooper.tac true [] [] ctxt
blanchet@56965
   120
    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
blanchet@55211
   121
blanchet@54828
   122
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
blanchet@56093
   123
  | string_of_play_outcome (Play_Timed_Out time) =
blanchet@56093
   124
    if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
blanchet@54828
   125
  | string_of_play_outcome Play_Failed = "failed"
blanchet@54828
   126
blanchet@55269
   127
fun play_outcome_ord (Played time1, Played time2) =
blanchet@55269
   128
    int_ord (pairself Time.toMilliseconds (time1, time2))
blanchet@55269
   129
  | play_outcome_ord (Played _, _) = LESS
blanchet@55269
   130
  | play_outcome_ord (_, Played _) = GREATER
blanchet@55269
   131
  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
blanchet@55269
   132
    int_ord (pairself Time.toMilliseconds (time1, time2))
blanchet@55269
   133
  | play_outcome_ord (Play_Timed_Out _, _) = LESS
blanchet@55269
   134
  | play_outcome_ord (_, Play_Timed_Out _) = GREATER
blanchet@55269
   135
  | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
blanchet@55269
   136
blanchet@55211
   137
fun apply_on_subgoal _ 1 = "by "
blanchet@55211
   138
  | apply_on_subgoal 1 _ = "apply "
blanchet@55211
   139
  | apply_on_subgoal i n =
blanchet@55211
   140
    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
blanchet@55211
   141
blanchet@55285
   142
(* FIXME *)
blanchet@56985
   143
fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
blanchet@56985
   144
  apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth
blanchet@55211
   145
blanchet@56093
   146
fun try_command_line banner play command =
blanchet@56093
   147
  let val s = string_of_play_outcome play in
blanchet@56093
   148
    banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
blanchet@56093
   149
    (s |> s <> "" ? enclose " (" ")") ^ "."
blanchet@56093
   150
  end
smolkas@52555
   151
blanchet@55211
   152
fun minimize_line _ [] = ""
blanchet@55211
   153
  | minimize_line minimize_command ss =
blanchet@55211
   154
    (case minimize_command ss of
blanchet@55211
   155
      "" => ""
blanchet@55211
   156
    | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
blanchet@55211
   157
blanchet@55211
   158
fun split_used_facts facts =
blanchet@55211
   159
  facts
blanchet@55211
   160
  |> List.partition (fn (_, (sc, _)) => sc = Chained)
blanchet@55211
   161
  |> pairself (sort_distinct (string_ord o pairself fst))
blanchet@55211
   162
blanchet@56985
   163
fun one_line_proof_text ctxt num_chained
blanchet@55285
   164
    ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
blanchet@55211
   165
  let
blanchet@55211
   166
    val (chained, extra) = split_used_facts used_facts
blanchet@55211
   167
blanchet@55211
   168
    val try_line =
blanchet@55211
   169
      map fst extra
blanchet@56985
   170
      |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
blanchet@56093
   171
      |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
blanchet@56093
   172
          else try_command_line banner play)
blanchet@55211
   173
  in
blanchet@55211
   174
    try_line ^ minimize_line minimize_command (map fst (extra @ chained))
blanchet@55211
   175
  end
smolkas@52555
   176
blanchet@54495
   177
end;