# HG changeset patch # User blanchet # Date 1284637481 -7200 # Node ID acb25e9cf6fb9da92d16ac2958c30d04acb2b9d7 # Parent 1740a2d6bef9555a41757ada0d772b97054250de factor out the inverse of "nice_atp_problem" diff -r 1740a2d6bef9 -r acb25e9cf6fb src/HOL/Tools/ATP/atp_proof.ML --- 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)\(, , \). The 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: . *) -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: [0:] || -> . *) -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; diff -r 1740a2d6bef9 -r acb25e9cf6fb src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 11:59:45 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 13:44:41 2010 +0200 @@ -88,8 +88,7 @@ | add_fact _ _ = I fun used_facts_in_tstplike_proof axiom_names = - atp_proof_from_tstplike_string Symtab.empty - #> rpair [] #-> fold (add_fact axiom_names) + atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names) fun used_facts axiom_names = used_facts_in_tstplike_proof axiom_names @@ -525,12 +524,24 @@ ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names) deps ([], []))) +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 s = + if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then + "c_equal" (* seen in Vampire proofs *) + else + s + fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor tstplike_proof conjecture_shape axiom_names params frees = let val lines = tstplike_proof - |> atp_proof_from_tstplike_string pool + |> atp_proof_from_tstplike_string + |> nasty_atp_proof pool + |> map_term_names_in_atp_proof repair_name |> decode_lines ctxt full_types tfrees |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) |> rpair [] |-> fold_rev add_nontrivial_line