# HG changeset patch # User blanchet # Date 1391442838 -3600 # Node ID ffa30623931696c9566a35b080eebb7acc24af78 # Parent 7bbbd9393ce0c444d367efd7574f2ff7ca4cd9ee renamed ML file diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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, diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Sledgehammer.thy --- 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" diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer.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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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) diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- /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; diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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 diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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) diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- 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;