--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 14:10:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 14:21:17 2013 +0100
@@ -36,9 +36,7 @@
UnknownError of string
type step_name = string * string list
-
- datatype 'a step =
- Inference_Step of step_name * formula_role * 'a * string * step_name list
+ type 'a step = step_name * formula_role * 'a * string * step_name list
type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
@@ -209,13 +207,10 @@
| (SOME i, SOME j) => int_ord (i, j)
end
-datatype 'a step =
- Inference_Step of step_name * formula_role * 'a * string * step_name list
+type 'a step = 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 (Inference_Step (name, _, _, _, _)) = name
-
(**** PARSING OF TSTP FORMAT ****)
(* Strings enclosed in single quotes (e.g., file names) *)
@@ -418,16 +413,14 @@
phi), "", [])
| Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
fun mk_step () =
- Inference_Step (name, role_of_tptp_string role, phi, rule,
- map (rpair []) deps)
+ (name, role_of_tptp_string role, phi, rule, map (rpair []) deps)
in
case role_of_tptp_string role of
Definition =>
(case phi of
AAtom (ATerm (("equal", []), _)) =>
(* Vampire's equality proxy axiom *)
- Inference_Step (name, Definition, phi, rule,
- map (rpair []) deps)
+ (name, Definition, phi, rule, map (rpair []) deps)
| _ => mk_step ())
| _ => mk_step ()
end)
@@ -473,8 +466,7 @@
-- Scan.option (Scan.this_string "derived from formulae "
|-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
>> (fn ((((num, rule), deps), u), names) =>
- Inference_Step ((num, these names), Unknown, u, rule,
- map (rpair []) deps))) x
+ ((num, these names), Unknown, u, rule, map (rpair []) deps))) x
val satallax_coreN = "__satallax_core" (* arbitrary *)
val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
@@ -483,14 +475,12 @@
fun parse_z3_tptp_line x =
(scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
>> (fn (name, names) =>
- Inference_Step (("", name :: names), Unknown, dummy_phi,
- z3_tptp_coreN, []))) x
+ (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x
(* Syntax: <name> *)
fun parse_satallax_line x =
(scan_general_id --| Scan.option ($$ " ")
- >> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN,
- []))) x
+ >> (fn s => ((s, [s]), Unknown, dummy_phi, satallax_coreN, []))) x
fun parse_line problem =
parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
@@ -507,13 +497,12 @@
| atp_proof_from_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
- |> sort (step_name_ord o pairself step_name)
+ |> sort (step_name_ord o pairself #1)
fun clean_up_dependencies _ [] = []
- | 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) ::
+ | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
+ (name, role, u, rule,
+ map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
clean_up_dependencies (name :: seen) steps
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
@@ -525,8 +514,8 @@
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 (Inference_Step (name, role, phi, rule, deps)) =
- Inference_Step (name, role, do_formula phi, rule, deps)
+ fun do_step (name, role, phi, rule, deps) =
+ (name, role, do_formula phi, rule, deps)
in map do_step end
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:10:51 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:21:17 2013 +0100
@@ -119,8 +119,7 @@
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
fun is_axiom_used_in_proof pred =
- exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
- | _ => false)
+ exists (fn ((_, ss), _, _, _, []) => exists pred ss)
fun lam_trans_from_atp_proof atp_proof default =
case (is_axiom_used_in_proof is_combinator_def atp_proof,
@@ -155,7 +154,7 @@
val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
val leo2_unfold_def_rule = "unfold_def"
-fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
+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
@@ -322,13 +321,13 @@
| aux t = t
in aux end
-fun decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
+fun decode_line sym_tab (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),
+ ((name, role, t, rule, deps),
fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
end
fun decode_lines ctxt sym_tab lines =
@@ -336,10 +335,8 @@
fun replace_one_dependency (old, new) dep =
if is_same_atp_step dep old then new else [dep]
-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 [])
+fun replace_dependencies_in_line p (name, role, t, rule, deps) =
+ (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
@@ -347,17 +344,16 @@
fun s_maybe_not role = role <> Conjecture ? s_not
-fun is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) =
- s_maybe_not role t aconv s_maybe_not role' t'
+fun is_same_inference (role, t) (_, 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 fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
- lines =
+fun add_line fact_names (name as (_, ss), role, t, rule, []) lines =
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or
definitions. *)
if is_conjecture ss then
- Inference_Step (name, role, t, rule, []) :: lines
+ (name, role, t, rule, []) :: lines
else if is_fact fact_names ss then
(* Facts are not proof lines. *)
if is_only_type_information t then
@@ -366,30 +362,30 @@
lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ (line as Inference_Step (name, role, t, _, _)) lines =
+ | add_line _ (line as (name, role, t, _, _)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
line :: lines
(* Is there a repetition? If so, replace later line by earlier one. *)
else case take_prefix (not o is_same_inference (role, t)) lines of
(_, []) => line :: lines
- | (pre, Inference_Step (name', _, _, _, _) :: post) =>
+ | (pre, (name', _, _, _, _) :: post) =>
line :: pre @ map (replace_dependencies_in_line (name', [name])) post
val waldmeister_conjecture_num = "1.0.0.0"
val repair_waldmeister_endgame =
let
- fun do_tail (Inference_Step (name, _, t, rule, deps)) =
- Inference_Step (name, Negated_Conjecture, s_not t, rule, deps)
+ fun do_tail (name, _, t, rule, deps) =
+ (name, Negated_Conjecture, s_not t, rule, deps)
fun do_body [] = []
- | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
+ | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
if num = waldmeister_conjecture_num then map do_tail (line :: lines)
else line :: do_body lines
in do_body end
(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
+fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
if is_only_type_information t then delete_dependency name lines
else line :: lines
| add_nontrivial_line line lines = line :: lines
@@ -408,8 +404,8 @@
val is_skolemize_rule =
member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
-fun add_desired_line fact_names frees
- (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
+fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps)
+ (j, lines) =
(j + 1,
if is_fact fact_names ss orelse
is_conjecture ss orelse
@@ -422,7 +418,7 @@
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 *)
+ (name, role, t, rule, deps) :: lines (* keep line *)
else
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
@@ -669,20 +665,19 @@
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
val conjs =
atp_proof |> map_filter
- (fn Inference_Step (name as (_, ss), _, _, _, []) =>
+ (fn (name as (_, ss), _, _, _, []) =>
if member (op =) ss conj_name then SOME name else NONE
| _ => NONE)
val assms =
atp_proof |> map_filter
- (fn Inference_Step (name as (_, ss), _, _, _, []) =>
+ (fn (name as (_, ss), _, _, _, []) =>
(case resolve_conjecture ss of
[j] =>
if j = length hyp_ts then NONE
else SOME (raw_label_for_name name, nth hyp_ts j)
| _ => NONE)
| _ => NONE)
- fun dep_of_step (Inference_Step (name, _, _, _, from)) =
- SOME (from, name)
+ fun dep_of_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
@@ -691,7 +686,7 @@
val bot = atp_proof |> List.last |> dep_of_step |> the |> snd
val steps =
Symtab.empty
- |> fold (fn Inference_Step (name as (s, _), role, t, rule, _) =>
+ |> fold (fn (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
s_maybe_not role