--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 17:12:58 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 17:37:35 2013 +0100
@@ -665,7 +665,7 @@
SMT_Solver.smt_tac ctxt thms
else if full then
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
- ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms
+ ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
else if String.isPrefix "metis (" (!reconstructor) then
let
val (type_encs, lam_trans) =
@@ -674,10 +674,10 @@
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
- ||> the_default ATP_Proof_Reconstruct.metis_default_lam_trans
+ ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
else if !reconstructor = "metis" then
- Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt
+ Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt
thms
else
K all_tac
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100
@@ -10,6 +10,7 @@
sig
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
+ type stature = ATP_Problem_Generate.stature
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
type 'a atp_proof = 'a ATP_Proof.atp_proof
@@ -23,7 +24,7 @@
val no_type_enc : string
val full_type_encs : string list
val partial_type_encs : string list
- val metis_default_lam_trans : string
+ val default_metis_lam_trans : string
val metis_call : string -> string -> string
val forall_of : term -> term -> term
val exists_of : term -> term -> term
@@ -35,6 +36,18 @@
Proof.context -> bool -> int Symtab.table ->
(string, string, (string, string) atp_term, string) atp_formula -> term
+ val resolve_fact : (string * 'a) list vector -> string list -> (string * 'a) list
+ val resolve_conjecture : string list -> int list
+ val is_fact : (string * 'a) list vector -> string list -> bool
+ val is_conjecture : string list -> bool
+ val used_facts_in_atp_proof :
+ 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 is_typed_helper_used_in_atp_proof : string atp_proof -> bool
val termify_atp_proof :
Proof.context -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
@@ -70,7 +83,7 @@
fun unalias_type_enc s =
AList.lookup (op =) type_enc_aliases s |> the_default [s]
-val metis_default_lam_trans = combsN
+val default_metis_lam_trans = combsN
fun metis_call type_enc lam_trans =
let
@@ -80,7 +93,7 @@
[alias] => alias
| _ => type_enc
val opts = [] |> type_enc <> partial_typesN ? cons type_enc
- |> lam_trans <> metis_default_lam_trans ? cons lam_trans
+ |> 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
@@ -345,6 +358,108 @@
| _ => raise ATP_FORMULA [phi]
in repair_tvar_sorts (do_formula true phi Vartab.empty) end
+fun find_first_in_list_vector vec key =
+ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+ | (_, value) => value) NONE vec
+
+val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+
+fun resolve_one_named_fact fact_names s =
+ case try (unprefix fact_prefix) s of
+ SOME s' =>
+ let val s' = s' |> unprefix_fact_number |> unascii_of in
+ s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
+ end
+ | NONE => NONE
+fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
+fun is_fact fact_names = not o null o resolve_fact fact_names
+
+fun resolve_one_named_conjecture s =
+ case try (unprefix conjecture_prefix) s of
+ SOME s' => Int.fromString s'
+ | NONE => NONE
+
+val resolve_conjecture = map_filter resolve_one_named_conjecture
+val is_conjecture = not o null o resolve_conjecture
+
+fun is_axiom_used_in_proof pred =
+ exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
+
+fun add_non_rec_defs fact_names accum =
+ Vector.foldl (fn (facts, facts') =>
+ union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
+ facts')
+ accum fact_names
+
+val isa_ext = Thm.get_name_hint @{thm ext}
+val isa_short_ext = Long_Name.base_name isa_ext
+
+fun ext_name ctxt =
+ if Thm.eq_thm_prop (@{thm ext},
+ singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
+ isa_short_ext
+ else
+ isa_ext
+
+val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
+val leo2_unfold_def_rule = "unfold_def"
+
+fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
+ (if rule = leo2_extcnf_equal_neg_rule then
+ insert (op =) (ext_name ctxt, (Global, General))
+ else if rule = leo2_unfold_def_rule then
+ (* LEO 1.3.3 does not record definitions properly, leading to missing
+ dependencies in the TSTP proof. Remove the next line once this is
+ fixed. *)
+ add_non_rec_defs fact_names
+ else if rule = agsyhol_coreN orelse rule = satallax_coreN then
+ (fn [] =>
+ (* agsyHOL and Satallax don't include definitions in their
+ unsatisfiable cores, so we assume the worst and include them all
+ here. *)
+ [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
+ | facts => facts)
+ else
+ I)
+ #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
+
+fun used_facts_in_atp_proof ctxt fact_names atp_proof =
+ if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
+ else fold (add_fact ctxt fact_names) atp_proof []
+
+fun used_facts_in_unsound_atp_proof _ _ [] = NONE
+ | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
+ let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
+ if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
+ not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
+ SOME (map fst used_facts)
+ else
+ NONE
+ end
+
+val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
+
+(* overapproximation (good enough) *)
+fun is_lam_lifted s =
+ String.isPrefix fact_prefix s andalso
+ String.isSubstring ascii_of_lam_fact_prefix s
+
+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
+
+val is_typed_helper_name =
+ String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
+fun is_typed_helper_used_in_atp_proof atp_proof =
+ is_axiom_used_in_proof is_typed_helper_name atp_proof
+
fun repair_name "$true" = "c_True"
| repair_name "$false" = "c_False"
| repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 19 17:12:58 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 19 17:37:35 2013 +0100
@@ -294,7 +294,7 @@
()
val (schem_facts, nonschem_facts) = List.partition has_tvar facts
val type_encs = override_type_encs |> the_default default_type_encs
- val lam_trans = lam_trans |> the_default metis_default_lam_trans
+ val lam_trans = lam_trans |> the_default default_metis_lam_trans
in
HEADGOAL (Method.insert_tac nonschem_facts THEN'
CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 17:12:58 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 17:37:35 2013 +0100
@@ -367,7 +367,7 @@
[]
else
[("type_enc", [hd (unalias_type_enc type_enc')])]) @
- (if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then
+ (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then
[]
else
[("lam_trans", [lam_trans'])])
@@ -820,7 +820,7 @@
bunch_of_reconstructors needs_full_types
(lam_trans_of_atp_proof atp_proof
o (fn desperate => if desperate then hide_lamsN
- else metis_default_lam_trans))
+ else default_metis_lam_trans))
in
(used_facts,
Lazy.lazy (fn () =>
@@ -838,19 +838,24 @@
Output.urgent_message "Generating proof text..."
else
()
- val atp_proof = (fn () => termify_atp_proof ctxt pool lifted sym_tab atp_proof)
- val isar_params =
- (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof,
- goal)
+ 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
+ val atp_proof = atp_proof |> termify_atp_proof ctxt pool lifted sym_tab
+ in
+ (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout,
+ isar_compress, isar_try0, fact_names, atp_proof, goal)
+ end
val one_line_params =
(preplay, proof_banner mode name, used_facts,
- choose_minimize_command ctxt params minimize_command name
- preplay,
+ choose_minimize_command ctxt params minimize_command name preplay,
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- proof_text ctxt isar_proofs isar_params
- num_chained one_line_params
+ proof_text ctxt isar_proofs isar_params num_chained one_line_params
end,
(if verbose then
"\nATP real CPU time: " ^ string_of_time run_time ^ "."
@@ -1048,7 +1053,7 @@
play_one_line_proof mode debug verbose preplay_timeout used_pairs
state subgoal SMT
(bunch_of_reconstructors false (fn desperate =>
- if desperate then liftingN else metis_default_lam_trans))),
+ if desperate then liftingN else default_metis_lam_trans))),
fn preplay =>
let
val one_line_params =
@@ -1082,7 +1087,7 @@
val reconstr =
if name = metisN then
Metis (type_enc |> the_default (hd partial_type_encs),
- lam_trans |> the_default metis_default_lam_trans)
+ lam_trans |> the_default default_metis_lam_trans)
else if name = smtN then
SMT
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100
@@ -13,22 +13,13 @@
type one_line_params = Sledgehammer_Reconstructor.one_line_params
type isar_params =
- bool * bool * Time.time option * real * bool * (string * stature) list vector
- * (unit -> (term, string) atp_step list) * thm
+ bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector
+ * (term, string) atp_step list * thm
- val lam_trans_of_atp_proof : string atp_proof -> string -> string
- val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
- val used_facts_in_atp_proof :
- 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 isar_proof_text :
Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text :
- Proof.context -> bool option -> isar_params -> int -> one_line_params
- -> string
+ Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string
end;
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
@@ -56,113 +47,6 @@
open String_Redirect
-(** fact extraction from ATP proofs **)
-
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
-val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
-
-fun resolve_one_named_fact fact_names s =
- case try (unprefix fact_prefix) s of
- SOME s' =>
- let val s' = s' |> unprefix_fact_number |> unascii_of in
- s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
- end
- | NONE => NONE
-fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
-fun is_fact fact_names = not o null o resolve_fact fact_names
-
-fun resolve_one_named_conjecture s =
- case try (unprefix conjecture_prefix) s of
- SOME s' => Int.fromString s'
- | NONE => NONE
-
-val resolve_conjecture = map_filter resolve_one_named_conjecture
-val is_conjecture = not o null o resolve_conjecture
-
-val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
-
-(* overapproximation (good enough) *)
-fun is_lam_lifted s =
- String.isPrefix fact_prefix s andalso
- String.isSubstring ascii_of_lam_fact_prefix s
-
-val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
-
-fun is_axiom_used_in_proof pred =
- exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
-
-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
-
-val is_typed_helper_name =
- String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
-
-fun is_typed_helper_used_in_atp_proof atp_proof =
- is_axiom_used_in_proof is_typed_helper_name atp_proof
-
-fun add_non_rec_defs fact_names accum =
- Vector.foldl (fn (facts, facts') =>
- union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
- facts')
- accum fact_names
-
-val isa_ext = Thm.get_name_hint @{thm ext}
-val isa_short_ext = Long_Name.base_name isa_ext
-
-fun ext_name ctxt =
- if Thm.eq_thm_prop (@{thm ext},
- singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
- isa_short_ext
- else
- isa_ext
-
-val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
-val leo2_unfold_def_rule = "unfold_def"
-
-fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
- (if rule = leo2_extcnf_equal_neg_rule then
- insert (op =) (ext_name ctxt, (Global, General))
- else if rule = leo2_unfold_def_rule then
- (* LEO 1.3.3 does not record definitions properly, leading to missing
- dependencies in the TSTP proof. Remove the next line once this is
- fixed. *)
- add_non_rec_defs fact_names
- else if rule = agsyhol_coreN orelse rule = satallax_coreN then
- (fn [] =>
- (* agsyHOL and Satallax don't include definitions in their
- unsatisfiable cores, so we assume the worst and include them all
- here. *)
- [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
- | facts => facts)
- else
- I)
- #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
-
-fun used_facts_in_atp_proof ctxt fact_names atp_proof =
- if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
- else fold (add_fact ctxt fact_names) atp_proof []
-
-fun used_facts_in_unsound_atp_proof _ _ [] = NONE
- | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
- let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
- if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
- not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
- SOME (map fst used_facts)
- else
- NONE
- end
-
-
-(** Isar proof construction and manipulation **)
-
val assume_prefix = "a"
val have_prefix = "f"
val raw_prefix = "x"
@@ -339,11 +223,12 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * real * bool * (string * stature) list vector
- * (unit -> (term, string) atp_step list) * thm
+ bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector
+ * (term, string) atp_step list * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, goal)
+ (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
+ isar_try0, fact_names, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -354,11 +239,6 @@
ctxt |> Variable.set_body false
|> Proof_Context.add_fixes fixes)
val one_line_proof = one_line_proof_text 0 one_line_params
- val atp_proof = atp_proof ()
- val type_enc =
- if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
- else partial_typesN
- val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
val do_preplay = preplay_timeout <> SOME Time.zeroTime
fun isar_proof_of () =
@@ -509,7 +389,7 @@
|> redirect_graph axioms tainted bot
|> isar_proof_of_direct_proof
|> relabel_proof_canonically
- |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay
+ |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout)
val ((preplay_time, preplay_fail), isar_proof) =
isar_proof
@@ -521,8 +401,8 @@
preplay_interface
|> `overall_preplay_stats
||> clean_up_labels_in_proof
- val isar_text = string_of_proof ctxt type_enc lam_trans subgoal
- subgoal_count isar_proof
+ val isar_text =
+ string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
in
case isar_text of
"" =>
@@ -572,7 +452,7 @@
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt isar_proofs isar_params
+ isar_proof_text ctxt isar_proofs (isar_params ())
else
one_line_proof_text num_chained) one_line_params