# HG changeset patch # User blanchet # Date 1308564823 -7200 # Node ID 51857e7fa64bbb59bd023fc38a71cc96c592451c # Parent 20593e9bbe38c1058a8058ededf7e772c8925888 clean up SPASS FLOTTER hack diff -r 20593e9bbe38 -r 51857e7fa64b src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 20 11:42:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 20 12:13:43 2011 +0200 @@ -35,7 +35,7 @@ InternalError | UnknownError of string - type step_name = string * string option + type step_name = string * string list option datatype 'a step = Definition of step_name * 'a * 'a | @@ -55,7 +55,8 @@ val scan_general_id : string list -> string * string list val parse_formula : string list -> (string, 'a, string fo_term) formula * string list - val atp_proof_from_tstplike_proof : string problem -> string -> string proof + val atp_proof_from_tstplike_proof : + string problem -> string -> string -> string proof val clean_up_atp_proof_dependencies : string proof -> string proof val map_term_names_in_atp_proof : (string -> string) -> string proof -> string proof @@ -206,7 +207,7 @@ | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) | (tstplike_proof, _) => (tstplike_proof, NONE) -type step_name = string * string option +type step_name = string * string list option fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 @@ -387,7 +388,7 @@ fun find_formula_in_problem problem phi = problem |> maps snd |> map_filter (matching_formula_line_identifier phi) - |> try hd + |> try (single o hd) (* Syntax: (cnf|fof|tff|thf)\(, , \). @@ -410,7 +411,7 @@ else if s = waldmeister_conjecture then find_formula_in_problem problem (mk_anot phi) else - SOME (s |> perhaps (try (unprefix tofof_fact_prefix)))), + SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]), []) | ["file", _] => ((num, find_formula_in_problem problem phi), []) | _ => ((num, NONE), deps) @@ -455,27 +456,79 @@ -- Scan.repeat parse_decorated_atom >> (mk_horn o apfst (op @))) x +fun resolve_spass_num spass_names num = + case Int.fromString num of + SOME j => if j > 0 andalso j <= Vector.length spass_names then + SOME (Vector.sub (spass_names, j - 1)) + else + NONE + | NONE => NONE + (* Syntax: [0:] || -> . *) -fun parse_spass_line x = +fun parse_spass_line spass_names x = (scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." >> (fn ((num, deps), u) => - Inference ((num, NONE), u, map (rpair NONE) deps))) x + Inference ((num, resolve_spass_num spass_names num), u, + map (swap o `(resolve_spass_num spass_names)) deps))) x + +fun parse_line problem spass_names = + parse_tstp_line problem || parse_spass_line spass_names +fun parse_proof problem spass_names tstp = + tstp |> strip_spaces_except_between_ident_chars + |> raw_explode + |> Scan.finite Symbol.stopper + (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) + (Scan.repeat1 (parse_line problem spass_names)))) + |> fst + +(** SPASS's FLOTTER hack **) + +(* This is a hack required for keeping track of facts after they have been + clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is + also part of this hack. *) + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end -fun parse_line problem = parse_tstp_line problem || parse_spass_line -fun parse_proof problem s = - s |> strip_spaces_except_between_ident_chars - |> raw_explode - |> Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.repeat1 (parse_line problem)))) - |> fst +fun is_head_digit s = Char.isDigit (String.sub (s, 0)) +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.position "." #> fst #> Substring.string + #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation + #> fst -fun atp_proof_from_tstplike_proof _ "" = [] - | atp_proof_from_tstplike_proof problem s = - s ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - |> parse_proof problem +fun extract_spass_name_vector output = + (if String.isSubstring set_ClauseFormulaRelationN output then + let + val num_seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + val name_seq = num_seq |> map (these o AList.lookup (op =) name_map) + in name_seq end + else + []) + |> Vector.fromList + +fun atp_proof_from_tstplike_proof _ _ "" = [] + | atp_proof_from_tstplike_proof problem output tstp = + tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) + |> parse_proof problem (extract_spass_name_vector output) |> sort (step_name_ord o pairself step_name) fun clean_up_dependencies _ [] = [] diff -r 20593e9bbe38 -r 51857e7fa64b src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 20 11:42:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 20 12:13:43 2011 +0200 @@ -30,10 +30,6 @@ type isar_params = bool * bool * int * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof * thm - val repair_conjecture_shape_and_fact_names : - string -> int list list -> int -> (string * locality) list vector - -> int list - -> int list list * int * (string * locality) list vector * int list val used_facts_in_atp_proof : Proof.context -> int -> (string * locality) list vector -> string proof -> (string * locality) list @@ -82,9 +78,6 @@ bool * bool * int * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof * thm -fun is_head_digit s = Char.isDigit (String.sub (s, 0)) -val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) - val is_typed_helper_name = String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix @@ -92,78 +85,22 @@ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key | (_, value) => value) NONE vec - -(** SPASS's FLOTTER hack **) - -(* This is a hack required for keeping track of facts after they have been - clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is - also part of this hack. *) - -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" - -fun extract_clause_sequence output = - let - val tokens_of = String.tokens (not o Char.isAlphaNum) - fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) - | extract_num _ = NONE - in output |> split_lines |> map_filter (extract_num o tokens_of) end - -val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," - -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" - --| Scan.option ($$ ",") -val parse_clause_formula_relation = - Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" - |-- Scan.repeat parse_clause_formula_pair -val extract_clause_formula_relation = - Substring.full #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.position "." #> fst #> Substring.string - #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation - #> fst - val unprefix_fact_number = space_implode "_" o tl o space_explode "_" -fun repair_conjecture_shape_and_fact_names output conjecture_shape - fact_offset fact_names typed_helpers = - if String.isSubstring set_ClauseFormulaRelationN output then - let - val j0 = hd (hd conjecture_shape) - val seq = extract_clause_sequence output - val name_map = extract_clause_formula_relation output - fun renumber_conjecture j = - conjecture_prefix ^ string_of_int (j - j0) - |> AList.find (fn (s, ss) => member (op =) ss s) name_map - |> map (fn s => find_index (curry (op =) s) seq + 1) - fun names_for_number j = - j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unascii_of o unprefix_fact_number - o unprefix fact_prefix)) - |> map (fn name => - (name, name |> find_first_in_list_vector fact_names |> the) - handle Option.Option => - error ("No such fact: " ^ quote name ^ ".")) - in - (conjecture_shape |> map (maps renumber_conjecture), 0, - seq |> map names_for_number |> Vector.fromList, - name_map |> filter (forall is_typed_helper_name o snd) |> map fst) - end - else - (conjecture_shape, fact_offset, fact_names, typed_helpers) - val vampire_step_prefix = "f" (* grrr... *) val extract_step_number = Int.fromString o perhaps (try (unprefix vampire_step_prefix)) -fun resolve_fact _ fact_names (_, SOME s) = - (case try (unprefix fact_prefix) s of - SOME s' => - let val s' = s' |> unprefix_fact_number |> unascii_of in - case find_first_in_list_vector fact_names s' of - SOME x => [(s', x)] - | NONE => [] - end - | NONE => []) +fun resolve_one_named_fact fact_names s = + case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + s' |> find_first_in_list_vector fact_names |> Option.map (pair s') + end + | NONE => NONE +fun resolve_fact _ fact_names (_, SOME ss) = + map_filter (resolve_one_named_fact fact_names) ss | resolve_fact facts_offset fact_names (num, NONE) = (case extract_step_number num of SOME j => @@ -177,13 +114,13 @@ fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape -fun resolve_conjecture _ (_, SOME s) = - (case try (unprefix conjecture_prefix) s of - SOME s' => - (case Int.fromString s' of - SOME j => [j] - | NONE => []) - | NONE => []) +fun resolve_one_named_conjecture s = + case try (unprefix conjecture_prefix) s of + SOME s' => Int.fromString s' + | NONE => NONE + +fun resolve_conjecture _ (_, SOME ss) = + map_filter resolve_one_named_conjecture ss | resolve_conjecture conjecture_shape (num, NONE) = case extract_step_number num of SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of @@ -194,7 +131,7 @@ fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape -fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s +fun is_typed_helper _ (_, SOME ss) = exists is_typed_helper_name ss | is_typed_helper typed_helpers (num, NONE) = (case extract_step_number num of SOME i => member (op =) typed_helpers i diff -r 20593e9bbe38 -r 51857e7fa64b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 20 11:42:41 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 20 12:13:43 2011 +0200 @@ -678,16 +678,8 @@ val (atp_proof, outcome) = extract_tstplike_proof_and_outcome verbose complete proof_delims known_failures output - |>> atp_proof_from_tstplike_proof atp_problem + |>> atp_proof_from_tstplike_proof atp_problem output handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete) - val (conjecture_shape, facts_offset, fact_names, - typed_helpers) = - if is_none outcome then - repair_conjecture_shape_and_fact_names output - conjecture_shape facts_offset fact_names typed_helpers - else - (* don't bother repairing *) - (conjecture_shape, facts_offset, fact_names, typed_helpers) val outcome = case outcome of NONE =>