--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 11:59:45 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 13:44:41 2010 +0200
@@ -3,7 +3,7 @@
Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
-Abstract representation of ATP proofs and TSTP/SPASS/Vampire syntax.
+Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax.
*)
signature ATP_PROOF =
@@ -21,8 +21,10 @@
val step_num : step_name -> string
val is_same_step : step_name * step_name -> bool
- val atp_proof_from_tstplike_string :
- string Symtab.table -> string -> string proof
+ val atp_proof_from_tstplike_string : string -> string proof
+ val map_term_names_in_atp_proof :
+ (string -> string) -> string proof -> string proof
+ val nasty_atp_proof : string Symtab.table -> string proof -> string proof
end;
structure ATP_Proof : ATP_PROOF =
@@ -92,18 +94,6 @@
|| Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
-fun repair_name _ "$true" = "c_True"
- | repair_name _ "$false" = "c_False"
- | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
- | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
- | repair_name pool s =
- case Symtab.lookup pool s of
- SOME s' => s'
- | NONE =>
- if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
- "c_equal" (* seen in Vampire proofs *)
- else
- s
(* Generalized first-order terms, which include file names, numbers, etc. *)
fun parse_annotation strict x =
((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
@@ -123,18 +113,16 @@
fun parse_vampire_detritus x =
(scan_general_id |-- $$ ":" --| scan_general_id >> K []) x
-fun parse_term pool x =
- ((scan_general_id >> repair_name pool)
- -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
+fun parse_term x =
+ (scan_general_id
+ -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
--| $$ ")") []
--| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
>> ATerm) x
-and parse_terms pool x =
- (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
+and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
-fun parse_atom pool =
- parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
- -- parse_term pool)
+val parse_atom =
+ parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
>> (fn (u1, NONE) => AAtom u1
| (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
| (u1, SOME (SOME _, u2)) =>
@@ -144,20 +132,19 @@
(* TPTP formulas are fully parenthesized, so we don't need to worry about
operator precedence. *)
-fun parse_formula pool x =
- (($$ "(" |-- parse_formula pool --| $$ ")"
+fun parse_formula x =
+ (($$ "(" |-- parse_formula --| $$ ")"
|| ($$ "!" >> K AForall || $$ "?" >> K AExists)
- --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
- -- parse_formula pool
+ --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
>> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
- || $$ "~" |-- parse_formula pool >> mk_anot
- || parse_atom pool)
+ || $$ "~" |-- parse_formula >> mk_anot
+ || parse_atom)
-- Scan.option ((Scan.this_string "=>" >> K AImplies
|| Scan.this_string "<=>" >> K AIff
|| Scan.this_string "<~>" >> K ANotIff
|| Scan.this_string "<=" >> K AIf
|| $$ "|" >> K AOr || $$ "&" >> K AAnd)
- -- parse_formula pool)
+ -- parse_formula)
>> (fn (phi1, NONE) => phi1
| (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
@@ -167,34 +154,34 @@
(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
The <num> could be an identifier, but we assume integers. *)
- fun parse_tstp_line pool =
- ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
- |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
- -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
- >> (fn (((num, role), phi), deps) =>
- let
- val (name, deps) =
- case deps of
- ["file", _, s] => (Str (num, s), [])
- | _ => (Num num, deps)
- in
- case role of
- "definition" =>
- (case phi of
- AConn (AIff, [phi1 as AAtom _, phi2]) =>
- Definition (name, phi1, phi2)
- | AAtom (ATerm ("c_equal", _)) =>
- (* Vampire's equality proxy axiom *)
- Inference (name, phi, map Num deps)
- | _ => raise Fail "malformed definition")
- | _ => Inference (name, phi, map Num deps)
- end)
+val parse_tstp_line =
+ ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
+ |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
+ -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
+ >> (fn (((num, role), phi), deps) =>
+ let
+ val (name, deps) =
+ case deps of
+ ["file", _, s] => (Str (num, s), [])
+ | _ => (Num num, deps)
+ in
+ case role of
+ "definition" =>
+ (case phi of
+ AConn (AIff, [phi1 as AAtom _, phi2]) =>
+ Definition (name, phi1, phi2)
+ | AAtom (ATerm ("c_equal", _)) =>
+ (* Vampire's equality proxy axiom *)
+ Inference (name, phi, map Num deps)
+ | _ => raise Fail "malformed definition")
+ | _ => Inference (name, phi, map Num deps)
+ end)
(**** PARSING OF VAMPIRE OUTPUT ****)
(* Syntax: <num>. <formula> <annotation> *)
-fun parse_vampire_line pool =
- scan_general_id --| $$ "." -- parse_formula pool -- parse_annotation true
+val parse_vampire_line =
+ scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
>> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
(**** PARSING OF SPASS OUTPUT ****)
@@ -209,8 +196,8 @@
(* It is not clear why some literals are followed by sequences of stars and/or
pluses. We ignore them. *)
-fun parse_decorated_atom pool =
- parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
+val parse_decorated_atom =
+ parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
| mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
@@ -219,26 +206,24 @@
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
foldr1 (mk_aconn AOr) pos_lits)
-fun parse_horn_clause pool =
- Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
- -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
- -- Scan.repeat (parse_decorated_atom pool)
+val parse_horn_clause =
+ Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
+ -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
+ -- Scan.repeat parse_decorated_atom
>> (mk_horn o apfst (op @))
(* Syntax: <num>[0:<inference><annotations>]
<atoms> || <atoms> -> <atoms>. *)
-fun parse_spass_line pool =
+val parse_spass_line =
scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
- -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
+ -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
>> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
-fun parse_line pool =
- parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
-fun parse_lines pool = Scan.repeat1 (parse_line pool)
-fun parse_proof pool =
+val parse_line = parse_tstp_line || parse_vampire_line || parse_spass_line
+val parse_proof =
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
- (parse_lines pool)))
+ (Scan.repeat1 parse_line)))
o explode o strip_spaces_except_between_ident_chars (*### FIXME: why isn't strip_spaces enough?*)
fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
@@ -249,10 +234,29 @@
Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
clean_up_dependencies (name :: seen) steps
-fun atp_proof_from_tstplike_string pool =
+val atp_proof_from_tstplike_string =
suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
- #> parse_proof pool
+ #> parse_proof
#> sort (step_name_ord o pairself step_name)
#> clean_up_dependencies []
+fun map_term_names_in_term f (ATerm (s, ts)) =
+ ATerm (f s, map (map_term_names_in_term f) ts)
+fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
+ AQuant (q, xs, map_term_names_in_formula f phi)
+ | map_term_names_in_formula f (AConn (c, phis)) =
+ AConn (c, map (map_term_names_in_formula f) phis)
+ | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
+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)
+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
+fun nasty_atp_proof pool =
+ if Symtab.is_empty pool then I
+ else map_term_names_in_atp_proof (nasty_name pool)
+
end;