1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3    Author:     Steffen Juilf Smolka, TU Muenchen
4
5Reconstructors.
6*)
7
8signature SLEDGEHAMMER_PROOF_METHODS =
9sig
10  type stature = ATP_Problem_Generate.stature
11
12  datatype proof_method =
13    Metis_Method of string option * string option |
14    Meson_Method |
15    SMT_Method |
16    SATx_Method |
17    Blast_Method |
18    Simp_Method |
19    Simp_Size_Method |
20    Auto_Method |
21    Fastforce_Method |
22    Force_Method |
23    Moura_Method |
24    Linarith_Method |
25    Presburger_Method |
26    Algebra_Method
27
28  datatype play_outcome =
29    Played of Time.time |
30    Play_Timed_Out of Time.time |
31    Play_Failed
32
33  type one_line_params =
34    ((string * stature) list * (proof_method * play_outcome)) * string * int * int
35
36  val is_proof_method_direct : proof_method -> bool
37  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
38  val string_of_proof_method : Proof.context -> string list -> proof_method -> string
39  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
40  val string_of_play_outcome : play_outcome -> string
41  val play_outcome_ord : play_outcome ord
42  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
43end;
44
45structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
46struct
47
48open ATP_Util
49open ATP_Problem_Generate
50open ATP_Proof_Reconstruct
51
52datatype proof_method =
53  Metis_Method of string option * string option |
54  Meson_Method |
55  SMT_Method |
56  SATx_Method |
57  Blast_Method |
58  Simp_Method |
59  Simp_Size_Method |
60  Auto_Method |
61  Fastforce_Method |
62  Force_Method |
63  Moura_Method |
64  Linarith_Method |
65  Presburger_Method |
66  Algebra_Method
67
68datatype play_outcome =
69  Played of Time.time |
70  Play_Timed_Out of Time.time |
71  Play_Failed
72
73type one_line_params =
74  ((string * stature) list * (proof_method * play_outcome)) * string * int * int
75
76fun is_proof_method_direct (Metis_Method _) = true
77  | is_proof_method_direct Meson_Method = true
78  | is_proof_method_direct SMT_Method = true
79  | is_proof_method_direct Simp_Method = true
80  | is_proof_method_direct Simp_Size_Method = true
81  | is_proof_method_direct _ = false
82
83fun proof_method_distinguishes_chained_and_direct Simp_Method = true
84  | proof_method_distinguishes_chained_and_direct Simp_Size_Method = true
85  | proof_method_distinguishes_chained_and_direct _ = false
86
87fun is_proof_method_multi_goal Auto_Method = true
88  | is_proof_method_multi_goal _ = false
89
90fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
91
92fun string_of_proof_method ctxt ss meth =
93  let
94    val meth_s =
95      (case meth of
96        Metis_Method (NONE, NONE) => "metis"
97      | Metis_Method (type_enc_opt, lam_trans_opt) =>
98        "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
99      | Meson_Method => "meson"
100      | SMT_Method => "smt"
101      | SATx_Method => "satx"
102      | Blast_Method => "blast"
103      | Simp_Method => if null ss then "simp" else "simp add:"
104      | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
105      | Auto_Method => "auto"
106      | Fastforce_Method => "fastforce"
107      | Force_Method => "force"
108      | Moura_Method => "moura"
109      | Linarith_Method => "linarith"
110      | Presburger_Method => "presburger"
111      | Algebra_Method => "algebra")
112  in
113    maybe_paren (space_implode " " (meth_s :: ss))
114  end
115
116fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
117  (case meth of
118    Metis_Method (type_enc_opt, lam_trans_opt) =>
119    let
120      val ctxt = ctxt
121        |> Config.put Metis_Tactic.verbose false
122        |> Config.put Metis_Tactic.trace false
123    in
124      SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
125        global_facts) ctxt local_facts)
126    end
127  | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts)
128  | _ =>
129    Method.insert_tac ctxt local_facts THEN'
130    (case meth of
131      Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
132    | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
133    | Simp_Size_Method =>
134      Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
135    | _ =>
136      Method.insert_tac ctxt global_facts THEN'
137      (case meth of
138        SATx_Method => SAT.satx_tac ctxt
139      | Blast_Method => blast_tac ctxt
140      | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
141      | Fastforce_Method => Clasimp.fast_force_tac ctxt
142      | Force_Method => Clasimp.force_tac ctxt
143      | Moura_Method => moura_tac ctxt
144      | Linarith_Method => Lin_Arith.tac ctxt
145      | Presburger_Method => Cooper.tac true [] [] ctxt
146      | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
147
148fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
149  | string_of_play_outcome (Play_Timed_Out time) =
150    if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
151  | string_of_play_outcome Play_Failed = "failed"
152
153fun play_outcome_ord (Played time1, Played time2) =
154    int_ord (apply2 Time.toMilliseconds (time1, time2))
155  | play_outcome_ord (Played _, _) = LESS
156  | play_outcome_ord (_, Played _) = GREATER
157  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
158    int_ord (apply2 Time.toMilliseconds (time1, time2))
159  | play_outcome_ord (Play_Timed_Out _, _) = LESS
160  | play_outcome_ord (_, Play_Timed_Out _) = GREATER
161  | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
162
163fun apply_on_subgoal _ 1 = "by "
164  | apply_on_subgoal 1 _ = "apply "
165  | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
166
167(* FIXME *)
168fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
169  let
170    val (indirect_ss, direct_ss) =
171      if is_proof_method_direct meth then
172        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
173      else
174        (extras, [])
175  in
176    (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
177    apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^
178    (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
179  end
180
181fun try_command_line banner play command =
182  let val s = string_of_play_outcome play in
183    banner ^ ": " ^ Active.sendback_markup_command command ^
184    (s |> s <> "" ? enclose " (" ")")
185  end
186
187fun one_line_proof_text ctxt num_chained
188    ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
189  let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
190    map fst extra
191    |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
192    |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: "
193        else try_command_line banner play)
194  end
195
196end;
197