--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 13:44:41 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 13:52:17 2010 +0200
@@ -11,7 +11,7 @@
type 'a fo_term = 'a ATP_Problem.fo_term
type 'a uniform_formula = 'a ATP_Problem.uniform_formula
- datatype step_name = Str of string * string | Num of string
+ type step_name = string * string option
datatype 'a step =
Definition of step_name * 'a * 'a |
@@ -19,7 +19,6 @@
type 'a proof = 'a uniform_formula step list
- val step_num : step_name -> string
val is_same_step : step_name * step_name -> bool
val atp_proof_from_tstplike_string : string -> string proof
val map_term_names_in_atp_proof :
@@ -58,15 +57,12 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
-datatype step_name = Str of string * string | Num of string
+type step_name = string * string option
-fun step_num (Str (num, _)) = num
- | step_num (Num num) = num
-
-val is_same_step = op = o pairself step_num
+fun is_same_step p = p |> pairself fst |> op =
fun step_name_ord p =
- let val q = pairself step_num p in
+ let val q = pairself fst p in
(* The "unprefix" part is to cope with remote Vampire's output. The proper
solution would be to perform a topological sort, e.g. using the nice
"Graph" functor. *)
@@ -162,8 +158,8 @@
let
val (name, deps) =
case deps of
- ["file", _, s] => (Str (num, s), [])
- | _ => (Num num, deps)
+ ["file", _, s] => ((num, SOME s), [])
+ | _ => ((num, NONE), deps)
in
case role of
"definition" =>
@@ -172,9 +168,9 @@
Definition (name, phi1, phi2)
| AAtom (ATerm ("c_equal", _)) =>
(* Vampire's equality proxy axiom *)
- Inference (name, phi, map Num deps)
+ Inference (name, phi, map (rpair NONE) deps)
| _ => raise Fail "malformed definition")
- | _ => Inference (name, phi, map Num deps)
+ | _ => Inference (name, phi, map (rpair NONE) deps)
end)
(**** PARSING OF VAMPIRE OUTPUT ****)
@@ -182,7 +178,8 @@
(* Syntax: <num>. <formula> <annotation> *)
val parse_vampire_line =
scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
- >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
+ >> (fn ((num, phi), deps) =>
+ Inference ((num, NONE), phi, map (rpair NONE) deps))
(**** PARSING OF SPASS OUTPUT ****)
@@ -217,7 +214,7 @@
val parse_spass_line =
scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
- >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
+ >> (fn ((num, deps), u) => Inference ((num, NONE), u, map (rpair NONE) deps))
val parse_line = parse_tstp_line || parse_vampire_line || parse_spass_line
val parse_proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 13:44:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 13:52:17 2010 +0200
@@ -68,13 +68,13 @@
"\nTo minimize the number of lemmas, try this: " ^
Markup.markup Markup.sendback command ^ "."
-fun resolve_axiom axiom_names (Str (_, s)) =
+fun resolve_axiom axiom_names ((_, SOME s)) =
(case strip_prefix_and_unascii axiom_prefix s of
SOME s' => (case find_first_in_list_vector axiom_names s' of
SOME x => [(s', x)]
| NONE => [])
| NONE => [])
- | resolve_axiom axiom_names (Num num) =
+ | resolve_axiom axiom_names (num, NONE) =
case Int.fromString num of
SOME j =>
if j > 0 andalso j <= Vector.length axiom_names then
@@ -152,17 +152,15 @@
val assum_prefix = "A"
val fact_prefix = "F"
-fun resolve_conjecture conjecture_shape (Str (num, s)) =
- let
- val k = case try (unprefix conjecture_prefix) s of
- SOME s => Int.fromString s |> the_default ~1
- | NONE => case Int.fromString num of
- SOME j => find_index (exists (curry (op =) j))
- conjecture_shape
- | NONE => ~1
- in if k >= 0 then [k] else [] end
- | resolve_conjecture conjecture_shape (Num num) =
- resolve_conjecture conjecture_shape (Str (num, "")) (* HACK *)
+fun resolve_conjecture conjecture_shape (num, s_opt) =
+ let
+ val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
+ SOME s => Int.fromString s |> the_default ~1
+ | NONE => case Int.fromString num of
+ SOME j => find_index (exists (curry (op =) j))
+ conjecture_shape
+ | NONE => ~1
+ in if k >= 0 then [k] else [] end
val is_axiom = not o null oo resolve_axiom
val is_conjecture = not o null oo resolve_conjecture
@@ -170,9 +168,9 @@
fun raw_label_for_name conjecture_shape name =
case resolve_conjecture conjecture_shape name of
[j] => (conjecture_prefix, j)
- | _ => case Int.fromString (step_num name) of
+ | _ => case Int.fromString (fst name) of
SOME j => (raw_prefix, j)
- | NONE => (raw_prefix ^ step_num name, 0)
+ | NONE => (raw_prefix ^ fst name, 0)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)