--- 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