--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 16:53:58 2014 +0100
@@ -459,8 +459,8 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE),
- Sledgehammer_Reconstructor.Play_Failed),
+ preplay = Lazy.value (Sledgehammer_Proof_Methods.Metis_Method (NONE, NONE),
+ Sledgehammer_Proof_Methods.Play_Failed),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
: Sledgehammer_Prover.prover_result,
--- a/src/HOL/Sledgehammer.thy Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Feb 03 16:53:58 2014 +0100
@@ -17,7 +17,7 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 16:53:58 2014 +0100
@@ -10,7 +10,7 @@
sig
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type minimize_command = Sledgehammer_Proof_Methods.minimize_command
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
@@ -33,7 +33,7 @@
open ATP_Problem_Generate
open Sledgehammer_Util
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_Minimize
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 16:53:58 2014 +0100
@@ -11,7 +11,7 @@
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
type stature = ATP_Problem_Generate.stature
- type one_line_params = Sledgehammer_Reconstructor.one_line_params
+ type one_line_params = Sledgehammer_Proof_Methods.one_line_params
val trace : bool Config.T
@@ -31,7 +31,7 @@
open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Compress
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 16:53:58 2014 +0100
@@ -19,7 +19,7 @@
struct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 16:53:58 2014 +0100
@@ -21,7 +21,7 @@
structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
struct
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 16:53:58 2014 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_ISAR_PREPLAY =
sig
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type proof_method = Sledgehammer_Isar_Proof.proof_method
type isar_step = Sledgehammer_Isar_Proof.isar_step
type isar_proof = Sledgehammer_Isar_Proof.isar_proof
@@ -36,7 +36,7 @@
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 16:53:58 2014 +0100
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_ISAR_PROOF =
sig
- type proof_method = Sledgehammer_Reconstructor.proof_method
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
type label = string * int
type facts = label list * string list (* local and global facts *)
@@ -58,7 +58,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Annotate
type label = string * int
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 03 16:53:58 2014 +0100
@@ -0,0 +1,201 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Reconstructors.
+*)
+
+signature SLEDGEHAMMER_PROOF_METHODS =
+sig
+ type stature = ATP_Problem_Generate.stature
+
+ datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
+
+ datatype play_outcome =
+ Played of Time.time |
+ Play_Timed_Out of Time.time |
+ Play_Failed |
+ Not_Played
+
+ type minimize_command = string list -> string
+ type one_line_params =
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+
+ val smtN : string
+
+ val string_of_proof_method : proof_method -> string
+ val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+ val string_of_play_outcome : play_outcome -> string
+ val play_outcome_ord : play_outcome * play_outcome -> order
+ val one_line_proof_text : int -> one_line_params -> string
+ val silence_proof_methods : bool -> Proof.context -> Proof.context
+end;
+
+structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
+struct
+
+open ATP_Util
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+
+datatype proof_method =
+ Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Algebra_Method
+
+datatype play_outcome =
+ Played of Time.time |
+ Play_Timed_Out of Time.time |
+ Play_Failed |
+ Not_Played
+
+type minimize_command = string list -> string
+type one_line_params =
+ (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+
+val smtN = "smt"
+
+fun string_of_proof_method meth =
+ (case meth of
+ Metis_Method (NONE, NONE) => "metis"
+ | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ | Meson_Method => "meson"
+ | SMT_Method => "smt"
+ | Simp_Method => "simp"
+ | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Arith_Method => "arith"
+ | Blast_Method => "blast"
+ | Algebra_Method => "algebra")
+
+fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
+ Method.insert_tac local_facts THEN'
+ (case meth of
+ Metis_Method (type_enc_opt, lam_trans_opt) =>
+ Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
+ (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+ | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | Meson_Method => Meson.meson_tac ctxt global_facts
+ | _ =>
+ Method.insert_tac global_facts THEN'
+ (case meth of
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+ | Auto_Method => K (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Arith_Method => Arith_Data.arith_tac ctxt
+ | Blast_Method => blast_tac ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+
+fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
+ | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
+ | string_of_play_outcome Play_Failed = "failed"
+ | string_of_play_outcome _ = "unknown"
+
+fun play_outcome_ord (Played time1, Played time2) =
+ int_ord (pairself Time.toMilliseconds (time1, time2))
+ | play_outcome_ord (Played _, _) = LESS
+ | play_outcome_ord (_, Played _) = GREATER
+ | play_outcome_ord (Not_Played, Not_Played) = EQUAL
+ | play_outcome_ord (Not_Played, _) = LESS
+ | play_outcome_ord (_, Not_Played) = GREATER
+ | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
+ int_ord (pairself Time.toMilliseconds (time1, time2))
+ | play_outcome_ord (Play_Timed_Out _, _) = LESS
+ | play_outcome_ord (_, Play_Timed_Out _) = GREATER
+ | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
+
+(* 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 command_call name [] =
+ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
+(* FIXME *)
+fun proof_method_command meth i n used_chaineds num_chained ss =
+ (* unusing_chained_facts used_chaineds num_chained ^ *)
+ apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
+
+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
+ ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+
+ val (failed, ext_time) =
+ (case play of
+ Played time => (false, (SOME (false, time)))
+ | Play_Timed_Out time => (false, SOME (true, time))
+ | Play_Failed => (true, NONE)
+ | Not_Played => (false, NONE))
+
+ val try_line =
+ map fst extra
+ |> proof_method_command meth 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
+
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+ exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
+ Try0.silence_methods debug
+ #> Config.put SMT_Config.verbose debug
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 16:53:58 2014 +0100
@@ -12,9 +12,9 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type proof_method = Sledgehammer_Reconstructor.proof_method
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
+ type minimize_command = Sledgehammer_Proof_Methods.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -101,7 +101,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 16:53:58 2014 +0100
@@ -31,7 +31,7 @@
open ATP_Proof_Reconstruct
open ATP_Systems
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar
open Sledgehammer_Prover
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 16:53:58 2014 +0100
@@ -8,8 +8,8 @@
signature SLEDGEHAMMER_PROVER_MINIMIZE =
sig
type stature = ATP_Problem_Generate.stature
- type proof_method = Sledgehammer_Reconstructor.proof_method
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
type prover = Sledgehammer_Prover.prover
@@ -44,7 +44,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 16:53:58 2014 +0100
@@ -38,7 +38,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 15:33:18 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Reconstructors.
-*)
-
-signature SLEDGEHAMMER_RECONSTRUCTOR =
-sig
- type stature = ATP_Problem_Generate.stature
-
- datatype proof_method =
- Metis_Method of string option * string option |
- Meson_Method |
- SMT_Method |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Algebra_Method
-
- datatype play_outcome =
- Played of Time.time |
- Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
-
- type minimize_command = string list -> string
- type one_line_params =
- (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
- val smtN : string
-
- val string_of_proof_method : proof_method -> string
- val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
- val string_of_play_outcome : play_outcome -> string
- val play_outcome_ord : play_outcome * play_outcome -> order
- val one_line_proof_text : int -> one_line_params -> string
- val silence_proof_methods : bool -> Proof.context -> Proof.context
-end;
-
-structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
-struct
-
-open ATP_Util
-open ATP_Problem_Generate
-open ATP_Proof_Reconstruct
-
-datatype proof_method =
- Metis_Method of string option * string option |
- Meson_Method |
- SMT_Method |
- Simp_Method |
- Simp_Size_Method |
- Auto_Method |
- Fastforce_Method |
- Force_Method |
- Arith_Method |
- Blast_Method |
- Algebra_Method
-
-datatype play_outcome =
- Played of Time.time |
- Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
-
-type minimize_command = string list -> string
-type one_line_params =
- (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
-
-val smtN = "smt"
-
-fun string_of_proof_method meth =
- (case meth of
- Metis_Method (NONE, NONE) => "metis"
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
- | Meson_Method => "meson"
- | SMT_Method => "smt"
- | Simp_Method => "simp"
- | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
- | Auto_Method => "auto"
- | Fastforce_Method => "fastforce"
- | Force_Method => "force"
- | Arith_Method => "arith"
- | Blast_Method => "blast"
- | Algebra_Method => "algebra")
-
-fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac local_facts THEN'
- (case meth of
- Metis_Method (type_enc_opt, lam_trans_opt) =>
- Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
- (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
- | Meson_Method => Meson.meson_tac ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
- (case meth of
- Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Arith_Method => Arith_Data.arith_tac ctxt
- | Blast_Method => blast_tac ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
-
-fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
- | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
- | string_of_play_outcome Play_Failed = "failed"
- | string_of_play_outcome _ = "unknown"
-
-fun play_outcome_ord (Played time1, Played time2) =
- int_ord (pairself Time.toMilliseconds (time1, time2))
- | play_outcome_ord (Played _, _) = LESS
- | play_outcome_ord (_, Played _) = GREATER
- | play_outcome_ord (Not_Played, Not_Played) = EQUAL
- | play_outcome_ord (Not_Played, _) = LESS
- | play_outcome_ord (_, Not_Played) = GREATER
- | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
- int_ord (pairself Time.toMilliseconds (time1, time2))
- | play_outcome_ord (Play_Timed_Out _, _) = LESS
- | play_outcome_ord (_, Play_Timed_Out _) = GREATER
- | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
-
-(* 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 command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
-(* FIXME *)
-fun proof_method_command meth i n used_chaineds num_chained ss =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-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
- ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
-
- val (failed, ext_time) =
- (case play of
- Played time => (false, (SOME (false, time)))
- | Play_Timed_Out time => (false, SOME (true, time))
- | Play_Failed => (true, NONE)
- | Not_Played => (false, NONE))
-
- val try_line =
- map fst extra
- |> proof_method_command meth 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
-
-(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
- exceeded" warnings and the like. *)
-fun silence_proof_methods debug =
- Try0.silence_methods debug
- #> Config.put SMT_Config.verbose debug
-
-end;