--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 10:45:23 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 10:54:13 2013 +0100
@@ -38,7 +38,6 @@
type step_name = string * string list
datatype 'a step =
- Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * formula_role * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
@@ -211,13 +210,11 @@
end
datatype 'a step =
- Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * formula_role * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
-fun step_name (Definition_Step (name, _, _)) = name
- | step_name (Inference_Step (name, _, _, _, _)) = name
+fun step_name (Inference_Step (name, _, _, _, _)) = name
(**** PARSING OF TSTP FORMAT ****)
@@ -427,9 +424,7 @@
case role_of_tptp_string role of
Definition =>
(case phi of
- AConn (AIff, [phi1 as AAtom _, phi2]) =>
- Definition_Step (name, phi1, phi2)
- | AAtom (ATerm (("equal", []), _)) =>
+ AAtom (ATerm (("equal", []), _)) =>
(* Vampire's equality proxy axiom *)
Inference_Step (name, Definition, phi, rule,
map (rpair []) deps)
@@ -516,9 +511,6 @@
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen
- ((step as Definition_Step (name, _, _)) :: steps) =
- step :: clean_up_dependencies (name :: seen) steps
- | clean_up_dependencies seen
(Inference_Step (name, role, u, rule, deps) :: steps) =
Inference_Step (name, role, u, rule,
map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
@@ -533,9 +525,7 @@
AQuant (q, map (apfst f) xs, do_formula phi)
| do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
| do_formula (AAtom t) = AAtom (do_term t)
- fun do_step (Definition_Step (name, phi1, phi2)) =
- Definition_Step (name, do_formula phi1, do_formula phi2)
- | do_step (Inference_Step (name, role, phi, rule, deps)) =
+ fun do_step (Inference_Step (name, role, phi, rule, deps)) =
Inference_Step (name, role, do_formula phi, rule, deps)
in map do_step end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 10:45:23 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 10:54:13 2013 +0100
@@ -156,23 +156,22 @@
val leo2_unfold_def_rule = "unfold_def"
fun add_fact ctxt fact_names (Inference_Step ((_, 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 = satallax_coreN then
- (fn [] =>
- (* Satallax doesn't include definitions in its 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)
- | add_fact _ _ _ = I
+ (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 = satallax_coreN then
+ (fn [] =>
+ (* Satallax doesn't include definitions in its 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
@@ -299,9 +298,6 @@
else
s
-fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
- | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-
fun infer_formula_types ctxt =
Type.constraint HOLogic.boolT
#> Syntax.check_term
@@ -326,38 +322,21 @@
| aux t = t
in aux end
-fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t1 = prop_from_atp ctxt true sym_tab phi1
- val vars = snd (strip_comb t1)
- val frees = map unvarify_term vars
- val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = prop_from_atp ctxt true sym_tab phi2
- val (t1, t2) =
- HOLogic.eq_const HOLogic.typeT $ t1 $ t2
- |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
- |> HOLogic.dest_eq
- in
- (Definition_Step (name, t1, t2),
- fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
- end
- | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_from_atp ctxt true sym_tab
- |> uncombine_term thy |> infer_formula_types ctxt
- in
- (Inference_Step (name, role, t, rule, deps),
- fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
- end
+fun decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t = u |> prop_from_atp ctxt true sym_tab
+ |> uncombine_term thy |> infer_formula_types ctxt
+ in
+ (Inference_Step (name, role, t, rule, deps),
+ fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
+ end
fun decode_lines ctxt sym_tab lines =
fst (fold_map (decode_line sym_tab) lines ctxt)
fun replace_one_dependency (old, new) dep =
if is_same_atp_step dep old then new else [dep]
-fun replace_dependencies_in_line _ (line as Definition_Step _) = line
- | replace_dependencies_in_line p
+fun replace_dependencies_in_line p
(Inference_Step (name, role, t, rule, deps)) =
Inference_Step (name, role, t, rule,
fold (union (op =) o replace_one_dependency p) deps [])
@@ -368,14 +347,12 @@
fun s_maybe_not role = role <> Conjecture ? s_not
-fun is_same_inference _ (Definition_Step _) = false
- | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
+fun is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
s_maybe_not role t aconv s_maybe_not role' t'
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
-fun add_line _ (line as Definition_Step _) lines = line :: lines
- | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
+fun add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
lines =
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or
definitions. *)
@@ -389,7 +366,7 @@
lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines =
+ | add_line _ (line as Inference_Step (name, role, t, _, _)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
line :: lines
@@ -406,12 +383,10 @@
let
fun do_tail (Inference_Step (name, _, t, rule, deps)) =
Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
- | do_tail line = line
fun do_body [] = []
| do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
if num = waldmeister_conjecture_num then map do_tail (line :: lines)
else line :: do_body lines
- | do_body (line :: lines) = line :: do_body lines
in do_body end
(* Recursively delete empty lines (type information) from the proof. *)
@@ -434,25 +409,23 @@
val is_skolemize_rule =
member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
-fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
- (j, line :: map (replace_dependencies_in_line (name, [])) lines)
- | add_desired_line fact_names frees
+fun add_desired_line fact_names frees
(Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
- (j + 1,
- if is_fact fact_names ss orelse
- is_conjecture ss orelse
- is_skolemize_rule rule orelse
- (* the last line must be kept *)
- j = 0 orelse
- (not (is_only_type_information t) andalso
- null (Term.add_tvars t []) andalso
- not (exists_subterm (is_bad_free frees) t) andalso
- length deps >= 2 andalso
- (* kill next to last line, which usually results in a trivial step *)
- j <> 1) then
- Inference_Step (name, role, t, rule, deps) :: lines (* keep line *)
- else
- map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
+ (j + 1,
+ if is_fact fact_names ss orelse
+ is_conjecture ss orelse
+ is_skolemize_rule rule orelse
+ (* the last line must be kept *)
+ j = 0 orelse
+ (not (is_only_type_information t) andalso
+ null (Term.add_tvars t []) andalso
+ not (exists_subterm (is_bad_free frees) t) andalso
+ length deps >= 2 andalso
+ (* kill next to last line, which usually results in a trivial step *)
+ j <> 1) then
+ Inference_Step (name, role, t, rule, deps) :: lines (* keep line *)
+ else
+ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
val indent_size = 2
@@ -709,9 +682,8 @@
else SOME (raw_label_for_name name, nth hyp_ts j)
| _ => NONE)
| _ => NONE)
- fun dep_of_step (Definition_Step _) = NONE
- | dep_of_step (Inference_Step (name, _, _, _, from)) =
- SOME (from, name)
+ fun dep_of_step (Inference_Step (name, _, _, _, from)) =
+ SOME (from, name)
val refute_graph =
atp_proof |> map_filter dep_of_step |> make_refute_graph
val axioms = axioms_of_refute_graph refute_graph conjs
@@ -720,8 +692,7 @@
val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
- |> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step (name as (s, _), role, t, rule, _) =>
+ |> fold (fn Inference_Step (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
s_maybe_not role