--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Oct 19 21:40:32 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Oct 19 21:40:32 2011 +0200
@@ -39,7 +39,7 @@
datatype 'a step =
Definition of step_name * 'a * 'a |
- Inference of step_name * 'a * step_name list
+ Inference of step_name * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
@@ -223,12 +223,12 @@
datatype 'a step =
Definition of step_name * 'a * 'a |
- Inference of step_name * 'a * step_name list
+ Inference of step_name * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
fun step_name (Definition (name, _, _)) = name
- | step_name (Inference (name, _, _)) = name
+ | step_name (Inference (name, _, _, _)) = name
(**** PARSING OF TSTP FORMAT ****)
@@ -264,7 +264,7 @@
datatype source =
File_Source of string * string option |
- Inference_Source of string list
+ Inference_Source of string * string list
fun parse_dependencies x =
(scan_general_id ::: Scan.repeat ($$ "," |-- scan_general_id)) x
@@ -273,10 +273,9 @@
(Scan.this_string "file" |-- $$ "(" |-- scan_general_id --
Scan.option ($$ "," |-- scan_general_id) --| $$ ")"
>> File_Source
- || (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
- --| skip_formula --| $$ ",")
- ::: (skip_formula |-- $$ "," |-- $$ "[" |-- parse_dependencies --| $$ "]"
- --| $$ ")")
+ || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
+ --| skip_formula --| $$ "," --| skip_formula --| $$ "," --| $$ "["
+ -- parse_dependencies --| $$ "]" --| $$ ")"
>> Inference_Source) x
fun list_app (f, args) =
@@ -348,7 +347,7 @@
val parse_tstp_extra_arguments =
Scan.optional ($$ "," |-- parse_source
--| Scan.option ($$ "," |-- skip_formula))
- (Inference_Source [])
+ (Inference_Source ("", []))
val waldmeister_conjecture = "conjecture_1"
@@ -404,7 +403,7 @@
--| $$ "."
>> (fn (((num, role), phi), deps) =>
let
- val (name, deps) =
+ val (name, rule, deps) =
(* Waldmeister isn't exactly helping. *)
case deps of
File_Source (_, SOME s) =>
@@ -412,11 +411,11 @@
if s = waldmeister_conjecture then
find_formula_in_problem problem (mk_anot phi)
else
- SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]),
+ SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]), "",
[])
| File_Source _ =>
- ((num, find_formula_in_problem problem phi), [])
- | Inference_Source deps => ((num, NONE), deps)
+ ((num, find_formula_in_problem problem phi), "", [])
+ | Inference_Source (rule, deps) => ((num, NONE), rule, deps)
in
case role of
"definition" =>
@@ -425,9 +424,9 @@
Definition (name, phi1, phi2)
| AAtom (ATerm ("equal", _)) =>
(* Vampire's equality proxy axiom *)
- Inference (name, phi, map (rpair NONE) deps)
+ Inference (name, phi, rule, map (rpair NONE) deps)
| _ => raise UNRECOGNIZED_ATP_PROOF ())
- | _ => Inference (name, phi, map (rpair NONE) deps)
+ | _ => Inference (name, phi, rule, map (rpair NONE) deps)
end)
(**** PARSING OF SPASS OUTPUT ****)
@@ -468,16 +467,16 @@
(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
fun parse_spass_line spass_names =
- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+ scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" -- Symbol.scan_id
-- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
- >> (fn ((num, deps), u) =>
- Inference ((num, resolve_spass_num spass_names num), u,
+ >> (fn (((num, rule), deps), u) =>
+ Inference ((num, resolve_spass_num spass_names num), u, rule,
map (swap o `(resolve_spass_num spass_names)) deps))
(* Syntax: <name> *)
fun parse_satallax_line x =
(scan_general_id --| Scan.option ($$ " ")
- >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))) x
+ >> (fn s => Inference ((s, SOME [s]), dummy_phi, "", []))) x
fun parse_line problem spass_names =
parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
@@ -540,8 +539,8 @@
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
step :: clean_up_dependencies (name :: seen) steps
- | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
- Inference (name, u,
+ | clean_up_dependencies seen (Inference (name, u, rule, deps) :: steps) =
+ Inference (name, u, rule,
map_filter (fn dep => find_first (is_same_atp_step dep) seen)
deps) ::
clean_up_dependencies (name :: seen) steps
@@ -558,8 +557,8 @@
fun map_term_names_in_step f (Definition (name, phi1, phi2)) =
Definition (name, map_term_names_in_formula f phi1,
map_term_names_in_formula f phi2)
- | map_term_names_in_step f (Inference (name, phi, deps)) =
- Inference (name, map_term_names_in_formula f phi, deps)
+ | map_term_names_in_step f (Inference (name, phi, rule, deps)) =
+ Inference (name, map_term_names_in_formula f phi, rule, deps)
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Oct 19 21:40:32 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Oct 19 21:40:32 2011 +0200
@@ -148,13 +148,10 @@
else
isa_ext
-fun add_fact _ facts_offset fact_names (Inference (name, _, [])) =
+fun add_fact _ facts_offset fact_names (Inference (name, _, _, [])) =
union (op =) (resolve_fact facts_offset fact_names name)
- | add_fact ctxt _ _ (Inference (_, _, deps)) =
- if AList.defined (op =) deps leo2_ext then
- insert (op =) (ext_name ctxt, General)
- else
- I
+ | add_fact ctxt _ _ (Inference (_, _, rule, _)) =
+ if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
| add_fact _ _ _ _ = I
fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof =
@@ -162,7 +159,7 @@
else fold (add_fact ctxt facts_offset fact_names) atp_proof []
fun is_conjecture_used_in_proof conjecture_shape =
- exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
+ exists (fn Inference (name, _, _, []) => is_conjecture conjecture_shape name
| _ => false)
(* (quasi-)underapproximation of the truth *)
@@ -186,7 +183,7 @@
end
fun uses_typed_helpers typed_helpers =
- exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
+ exists (fn Inference (name, _, _, []) => is_typed_helper typed_helpers name
| _ => false)
@@ -558,16 +555,16 @@
(Definition (name, t1, t2),
fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
end
- | decode_line sym_tab (Inference (name, u, deps)) ctxt =
+ | decode_line sym_tab (Inference (name, u, rule, deps)) ctxt =
let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
- (Inference (name, t, deps),
+ (Inference (name, 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 is_same_inference _ (Definition _) = false
- | is_same_inference t (Inference (_, t', _)) = t aconv t'
+ | is_same_inference t (Inference (_, t', _, _)) = t aconv t'
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
@@ -576,13 +573,14 @@
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 _) = line
- | replace_dependencies_in_line p (Inference (name, t, deps)) =
- Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
+ | replace_dependencies_in_line p (Inference (name, t, rule, deps)) =
+ Inference (name, t, rule,
+ fold (union (op =) o replace_one_dependency p) deps [])
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
fun add_line _ _ (line as Definition _) lines = line :: lines
- | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
+ | add_line conjecture_shape fact_names (Inference (name, t, rule, [])) lines =
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or
definitions. *)
if is_fact fact_names name then
@@ -592,31 +590,31 @@
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference t) lines of
(_, []) => lines (* no repetition of proof line *)
- | (pre, Inference (name', _, _) :: post) =>
+ | (pre, Inference (name', _, _, _) :: post) =>
pre @ map (replace_dependencies_in_line (name', [name])) post
| _ => raise Fail "unexpected inference"
else if is_conjecture conjecture_shape name then
- Inference (name, s_not t, []) :: lines
+ Inference (name, s_not t, rule, []) :: lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ _ (Inference (name, t, deps)) lines =
+ | add_line _ _ (Inference (name, t, rule, deps)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
- Inference (name, t, deps) :: lines
+ Inference (name, t, rule, deps) :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference t) lines of
(* FIXME: Doesn't this code risk conflating proofs involving different
types? *)
- (_, []) => Inference (name, t, deps) :: lines
- | (pre, Inference (name', t', _) :: post) =>
- Inference (name, t', deps) ::
+ (_, []) => Inference (name, t, rule, deps) :: lines
+ | (pre, Inference (name', t', rule, _) :: post) =>
+ Inference (name, t', rule, deps) ::
pre @ map (replace_dependencies_in_line (name', [name])) post
| _ => raise Fail "unexpected inference"
(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (Inference (name, t, [])) lines =
+fun add_nontrivial_line (line as Inference (name, t, _, [])) lines =
if is_only_type_information t then delete_dependency name lines
- else Inference (name, t, []) :: lines
+ else line :: lines
| add_nontrivial_line line lines = line :: lines
and delete_dependency name lines =
fold_rev add_nontrivial_line
@@ -630,7 +628,7 @@
fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
(j, line :: map (replace_dependencies_in_line (name, [])) lines)
| add_desired_line isar_shrink_factor conjecture_shape fact_names frees
- (Inference (name, t, deps)) (j, lines) =
+ (Inference (name, t, rule, deps)) (j, lines) =
(j + 1,
if is_fact fact_names name orelse
is_conjecture conjecture_shape name orelse
@@ -642,7 +640,7 @@
length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
(* kill next to last line, which usually results in a trivial step *)
j <> 1) then
- Inference (name, t, deps) :: lines (* keep line *)
+ Inference (name, t, rule, deps) :: lines (* keep line *)
else
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
@@ -675,10 +673,10 @@
apfst (insert (op =) (raw_label_for_name conjecture_shape name))
fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
- | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) =
+ | step_for_line conjecture_shape _ _ _ (Inference (name, t, _, [])) =
Assume (raw_label_for_name conjecture_shape name, t)
| step_for_line conjecture_shape facts_offset fact_names j
- (Inference (name, t, deps)) =
+ (Inference (name, t, _, deps)) =
Have (if j = 1 then [Show] else [],
raw_label_for_name conjecture_shape name,
fold_rev forall_of (map Var (Term.add_vars t [])) t,