--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Feb 02 20:53:51 2014 +0100
@@ -41,7 +41,7 @@
Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->
'a atp_proof -> string list option
- val lam_trans_of_atp_proof : string atp_proof -> string -> string
+ val atp_proof_prefers_lifting : string atp_proof -> bool
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
('a, 'b) atp_step
@@ -90,8 +90,9 @@
(case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
[alias] => alias
| _ => type_enc)
- val opts = [] |> type_enc <> partial_typesN ? cons type_enc
- |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+ val opts =
+ [] |> type_enc <> partial_typesN ? cons type_enc
+ |> lam_trans <> default_metis_lam_trans ? cons lam_trans
in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
@@ -440,13 +441,9 @@
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
-fun lam_trans_of_atp_proof atp_proof default =
- (case (is_axiom_used_in_proof is_combinator_def atp_proof,
- is_axiom_used_in_proof is_lam_lifted atp_proof) of
- (false, false) => default
- | (false, true) => liftingN
-(* | (true, true) => combs_and_liftingN -- not supported by "metis" *)
- | (true, _) => combsN)
+fun atp_proof_prefers_lifting atp_proof =
+ (is_axiom_used_in_proof is_combinator_def atp_proof,
+ is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true)
val is_typed_helper_name =
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Feb 02 20:53:51 2014 +0100
@@ -174,8 +174,7 @@
Metis_KnuthBendixOrder.default
fun fall_back () =
(verbose_warning ctxt
- ("Falling back on " ^
- quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
+ ("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
in
(case filter (fn t => prop_of t aconv @{prop False}) cls of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Feb 02 20:53:51 2014 +0100
@@ -16,7 +16,8 @@
val trace : bool Config.T
type isar_params =
- bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+ bool * (string option * string option) * Time.time * real * bool
+ * (term, string) atp_step list * thm
val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
one_line_params -> string
@@ -108,26 +109,30 @@
end
type isar_params =
- bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+ bool * (string option * string option) * Time.time * real * bool * (term, string) atp_step list
+ * thm
val arith_methods =
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Algebra_Method, Metis_Method, Meson_Method]
+ Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
val datatype_methods = [Simp_Method, Simp_Size_Method]
-val metislike_methods =
- [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
- Force_Method, Algebra_Method, Meson_Method]
+val metislike_methods0 =
+ [Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
+ Fastforce_Method, Force_Method, Algebra_Method, Meson_Method]
val rewrite_methods =
- [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method, Meson_Method]
-val skolem_methods = [Metis_Method, Blast_Method, Meson_Method]
+ [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
+ Meson_Method]
+val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
fun isar_proof_text ctxt debug isar_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
fun isar_proof_of () =
let
- val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
- try0_isar, atp_proof, goal) = try isar_params ()
+ val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, atp_proof,
+ goal) = try isar_params ()
+
+ val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val (_, ctxt) =
@@ -265,8 +270,7 @@
and isar_proof outer fix assms lems infs =
Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
- val string_of_isar_proof =
- string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
+ val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count
val trace = Config.get ctxt trace
@@ -284,8 +288,7 @@
|> silence_reconstructors debug
val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
- preplay_data_of_isar_proof preplay_ctxt metis_type_enc metis_lam_trans preplay_timeout
- canonical_isar_proof
+ preplay_data_of_isar_proof preplay_ctxt preplay_timeout canonical_isar_proof
fun str_of_preplay_outcome outcome =
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sun Feb 02 20:53:51 2014 +0100
@@ -22,13 +22,13 @@
overall_preplay_outcome: isar_proof -> play_outcome}
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_data_of_isar_proof : Proof.context -> string -> string -> Time.time -> isar_proof ->
- isar_preplay_data
+ val preplay_data_of_isar_proof : Proof.context -> Time.time -> isar_proof -> isar_preplay_data
end;
structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
struct
+open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Reconstructor
open Sledgehammer_Isar_Proof
@@ -94,11 +94,13 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
+fun tac_of_method ctxt (local_facts, global_facts) meth =
Method.insert_tac local_facts THEN'
(case meth of
Meson_Method => Meson.meson_tac ctxt global_facts
- | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
+ | 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
| _ =>
Method.insert_tac global_facts THEN'
(case meth of
@@ -114,7 +116,7 @@
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
-fun raw_preplay_step type_enc lam_trans ctxt timeout meth
+fun raw_preplay_step ctxt timeout meth
(Prove (_, xs, _, t, subproofs, (fact_names, _))) =
let
val goal =
@@ -125,8 +127,8 @@
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
(* FIXME: generate fresh name *)
- val thesis = Free ("thesis", HOLogic.boolT)
- val thesis_prop = thesis |> HOLogic.mk_Trueprop
+ val thesis = Free ("thesis_preplay", HOLogic.boolT)
+ val thesis_prop = HOLogic.mk_Trueprop thesis
val frees = map Free xs
(* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
@@ -142,7 +144,7 @@
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
+ HEADGOAL (tac_of_method ctxt facts meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
val play_outcome = take_time timeout prove ()
@@ -169,10 +171,10 @@
(* Given a (canonically labeled) proof, produces an imperative preplay interface with a shared table
mapping from labels to preplay results. The preplay results are caluclated lazily and cached to
avoid repeated calculation. *)
-fun preplay_data_of_isar_proof ctxt type_enc lam_trans preplay_timeout proof =
+fun preplay_data_of_isar_proof ctxt preplay_timeout proof =
let
fun preplay_step timeout meth =
- try (raw_preplay_step type_enc lam_trans ctxt timeout meth)
+ try (raw_preplay_step ctxt timeout meth)
#> the_default Play_Failed
val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
@@ -14,8 +14,16 @@
datatype isar_qualifier = Show | Then
datatype proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+ Metis_Method of string option * string option |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Meson_Method |
+ Algebra_Method
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
@@ -50,7 +58,7 @@
val relabel_isar_proof_canonically : isar_proof -> isar_proof
val relabel_isar_proof_finally : isar_proof -> isar_proof
- val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
+ val string_of_isar_proof : Proof.context -> int -> int ->
(label -> proof_method list -> string) -> isar_proof -> string
end;
@@ -71,8 +79,16 @@
datatype isar_qualifier = Show | Then
datatype proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+ Metis_Method of string option * string option |
+ Simp_Method |
+ Simp_Size_Method |
+ Auto_Method |
+ Fastforce_Method |
+ Force_Method |
+ Arith_Method |
+ Blast_Method |
+ Meson_Method |
+ Algebra_Method
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
@@ -90,9 +106,11 @@
fun string_of_proof_method meth =
(case meth of
- Metis_Method => "metis"
+ Metis_Method (NONE, NONE) => "metis"
+ | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
| Simp_Method => "simp"
- | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
+ | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
| Auto_Method => "auto"
| Fastforce_Method => "fastforce"
| Force_Method => "force"
@@ -244,7 +262,7 @@
val indent_size = 2
-fun string_of_isar_proof ctxt type_enc lam_trans i n comment_of proof =
+fun string_of_isar_proof ctxt i n comment_of proof =
let
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt =
@@ -288,16 +306,24 @@
| with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
val using_facts = with_facts "" (enclose "using " " ")
- fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("(" ^ meth ^ " ") ")") ls ss
+
+ fun maybe_paren s = s |> String.isSubstring " " s ? enclose "(" ")"
+ fun by_facts meth ls ss =
+ "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss
+
+ fun is_direct_method (Metis_Method _) = true
+ | is_direct_method Meson_Method = true
+ | is_direct_method _ = false
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
arguably stylistically superior, because it emphasises the structure of the proof. It is also
more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
- fun of_method ls ss Metis_Method =
- using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
- | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
- | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_proof_method meth
+ fun of_method ls ss meth =
+ let val direct = is_direct_method meth in
+ using_facts ls (if direct then [] else ss) ^
+ by_facts (string_of_proof_method meth) [] (if direct then ss else [])
+ end
fun of_free (s, T) =
maybe_quote s ^ " :: " ^
@@ -360,7 +386,7 @@
(* One-step Metis proofs are pointless; better use the one-liner directly. *)
(case proof of
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
- | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method :: _))]) => ""
+ | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method _ :: _))]) => ""
| _ =>
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Feb 02 20:53:51 2014 +0100
@@ -344,8 +344,11 @@
val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val reconstrs =
- bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
- o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
+ bunch_of_reconstructors needs_full_types (fn desperate =>
+ if desperate then
+ if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN
+ else
+ default_metis_lam_trans)
in
(used_facts,
Lazy.lazy (fn () =>
@@ -359,16 +362,16 @@
fun isar_params () =
let
val metis_type_enc =
- if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
- else partial_typesN
- val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans
+ if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE
+ val metis_lam_trans =
+ if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
val atp_proof =
atp_proof
|> termify_atp_proof ctxt pool lifted sym_tab
|> introduce_spass_skolem
|> factify_atp_proof fact_names hyp_ts concl_t
in
- (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
+ (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
try0_isar, atp_proof, goal)
end
val one_line_params =