# HG changeset patch # User blanchet # Date 1272188326 -7200 # Node ID be73a2b2443b18c68d713734c0f04518297522d7 # Parent c00c57850eb739684b98f3153feb8016cf92bb41 support readable names even when Isar proof reconstruction is enabled -- useful for debugging diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Apr 25 11:38:46 2010 +0200 @@ -8,6 +8,7 @@ signature ATP_MANAGER = sig + type name_pool = Sledgehammer_HOL_Clause.name_pool type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -40,6 +41,7 @@ type prover_result = {outcome: failure option, message: string, + pool: name_pool option, relevant_thm_names: string list, atp_run_time_in_msecs: int, output: string, @@ -102,6 +104,7 @@ type prover_result = {outcome: failure option, message: string, + pool: name_pool option, relevant_thm_names: string list, atp_run_time_in_msecs: int, output: string, diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Apr 25 11:38:46 2010 +0200 @@ -88,6 +88,8 @@ | string_for_failure TimedOut = "Timed out." | string_for_failure OutOfResources = "The ATP ran out of resources." | string_for_failure OldSpass = + (* FIXME: Change the error message below to point to the Isabelle download + page once the package is there (around the Isabelle2010 release). *) "Warning: Sledgehammer requires a more recent version of SPASS with \ \support for the TPTP syntax. To install it, download and untar the \ \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ @@ -193,7 +195,7 @@ else "") ^ output) - val (((output, atp_run_time_in_msecs), res_code), _) = + val (((output, atp_run_time_in_msecs), res_code), pool) = with_path cleanup export run_on (prob_pathname subgoal); (* Check for success and print out some information on failure. *) @@ -201,12 +203,12 @@ extract_proof_and_outcome res_code proof_delims known_failures output val (message, relevant_thm_names) = case outcome of - NONE => proof_text isar_proof debug modulus sorts ctxt + NONE => proof_text isar_proof pool debug modulus sorts ctxt (minimize_command, proof, internal_thm_names, th, subgoal) | SOME failure => (string_for_failure failure ^ "\n", []) in - {outcome = outcome, message = message, + {outcome = outcome, message = message, pool = pool, relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = atp_run_time_in_msecs, output = output, proof = proof, internal_thm_names = internal_thm_names, @@ -228,7 +230,7 @@ higher_order follow_defs max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order false) - (write_tptp_file (debug andalso overlord andalso not isar_proof)) home + (write_tptp_file (debug andalso overlord)) home executable (arguments timeout) proof_delims known_failures name params minimize_command @@ -326,9 +328,6 @@ users have upgraded to 3.7, we can kill "spass" (and all DFG support in Sledgehammer) and rename "spass_tptp" "spass". *) -(* FIXME: Change the error message below to point to the Isabelle download - page once the package is there (around the Isabelle2010 release). *) - val spass_tptp_config = {home = #home spass_config, executable = #executable spass_config, diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Apr 25 11:38:46 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Author: Jia Meng, Cambridge University Computer Laboratory, NICTA + Author: Jasmin Blanchette, TU Muenchen *) signature SLEDGEHAMMER_FACT_FILTER = diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Sun Apr 25 11:38:46 2010 +0200 @@ -92,13 +92,14 @@ in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of - result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} => + result as {outcome = NONE, pool, internal_thm_names, filtered_clauses, + ...} => let val used = internal_thm_names |> Vector.foldr (op ::) [] |> sort_distinct string_ord val to_use = if length used < length name_thms_pairs then - filter (fn (name1, _) => List.exists (curry (op =) name1) used) + filter (fn (name1, _) => exists (curry (op =) name1) used) name_thms_pairs else name_thms_pairs val (min_thms, {proof, internal_thm_names, ...}) = @@ -109,7 +110,7 @@ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") in (SOME min_thms, - proof_text isar_proof debug modulus sorts ctxt + proof_text isar_proof pool debug modulus sorts ctxt (K "", proof, internal_thm_names, goal, i) |> fst) end | {outcome = SOME TimedOut, ...} => diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 11:38:46 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen Transformation of axiom rules (elim/intro/etc) into CNF forms. *) diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Sun Apr 25 11:38:46 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen Storing/printing FOL clauses and arity clauses. Typed equality is treated differently. diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sun Apr 25 11:38:46 2010 +0200 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER_HOL_CLAUSE = sig type name = Sledgehammer_FOL_Clause.name + type name_pool = Sledgehammer_FOL_Clause.name_pool type kind = Sledgehammer_FOL_Clause.kind type fol_type = Sledgehammer_FOL_Clause.fol_type type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause @@ -37,10 +38,10 @@ hol_clause list val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> unit + classrel_clause list * arity_clause list -> name_pool option val write_dfg_file : bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> unit + classrel_clause list * arity_clause list -> name_pool option end structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = @@ -500,7 +501,9 @@ fun write_tptp_file readable_names full_types explicit_apply file clauses = let fun section _ [] = [] - | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss + | section name ss = + "\n% " ^ name ^ plural_s (length ss) ^ " (" ^ Int.toString (length ss) ^ + ")\n" :: ss val pool = empty_name_pool readable_names val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses @@ -515,16 +518,16 @@ val arity_clss = map tptp_arity_clause arity_clauses val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) helper_clauses pool - in - File.write_list file - (header () :: - section "Relevant fact" ax_clss @ - section "Type variable" tfree_clss @ - section "Conjecture" conjecture_clss @ - section "Class relationship" classrel_clss @ - section "Arity declaration" arity_clss @ - section "Helper fact" helper_clss) - end + val _ = + File.write_list file + (header () :: + section "Relevant fact" ax_clss @ + section "Helper fact" helper_clss @ + section "Type variable" tfree_clss @ + section "Conjecture" conjecture_clss @ + section "Class relationship" classrel_clss @ + section "Arity declaration" arity_clss) + in pool end (* DFG format *) @@ -541,30 +544,30 @@ val params = (full_types, explicit_apply, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip - and probname = Path.implode (Path.base file) + and problem_name = Path.implode (Path.base file) val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) val (helper_clauses_strs, pool) = pool_map (apfst fst oo dfg_clause params) helper_clauses pool val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - in - File.write_list file - (header () :: - string_of_start probname :: - string_of_descrip probname :: - string_of_symbols (string_of_funcs funcs) - (string_of_preds (cl_preds @ ty_preds)) :: - "list_of_clauses(axioms, cnf).\n" :: - axstrs @ - map dfg_classrel_clause classrel_clauses @ - map dfg_arity_clause arity_clauses @ - helper_clauses_strs @ - ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ - tfree_clss @ - conjecture_clss @ - ["end_of_list.\n\n", - "end_problem.\n"]) - end + val _ = + File.write_list file + (header () :: + string_of_start problem_name :: + string_of_descrip problem_name :: + string_of_symbols (string_of_funcs funcs) + (string_of_preds (cl_preds @ ty_preds)) :: + "list_of_clauses(axioms, cnf).\n" :: + axstrs @ + map dfg_classrel_clause classrel_clauses @ + map dfg_arity_clause arity_clauses @ + helper_clauses_strs @ + ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ + tfree_clss @ + conjecture_clss @ + ["end_of_list.\n\n", + "end_problem.\n"]) + in pool end end; diff -r c00c57850eb7 -r be73a2b2443b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 10:22:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 11:38:46 2010 +0200 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig type minimize_command = string list -> string + type name_pool = Sledgehammer_FOL_Clause.name_pool val chained_hint: string val invert_const: string -> string @@ -20,11 +21,11 @@ minimize_command * string * string vector * thm * int -> string * string list val isar_proof_text: - bool -> int -> bool -> Proof.context + name_pool option -> bool -> int -> bool -> Proof.context -> minimize_command * string * string vector * thm * int -> string * string list val proof_text: - bool -> bool -> int -> bool -> Proof.context + bool -> name_pool option -> bool -> int -> bool -> Proof.context -> minimize_command * string * string vector * thm * int -> string * string list end; @@ -37,18 +38,23 @@ type minimize_command = string list -> string -val trace_proof_path = Path.basic "sledgehammer_trace_proof" - -fun trace_proof_msg f = - if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else (); - -fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); - fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" fun is_head_digit s = Char.isDigit (String.sub (s, 0)) fun is_axiom thm_names line_no = line_no <= Vector.length thm_names +fun ugly_name NONE s = s + | ugly_name (SOME the_pool) s = + case Symtab.lookup (snd the_pool) s of + SOME s' => s' + | NONE => s + +val trace_path = Path.basic "sledgehammer_proof_trace" +fun trace_proof_msg f = + if !trace then File.append (File.tmp_path trace_path) (f ()) else (); + +val string_of_thm = PrintMode.setmp [] o Display.string_of_thm + (**** PARSING OF TSTP FORMAT ****) (* Syntax trees, either term list or formulae *) @@ -66,52 +72,60 @@ val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) (* needed for SPASS's output format *) -fun fix_bool_literal "true" = "c_True" - | fix_bool_literal "false" = "c_False" -fun fix_symbol "equal" = "c_equal" - | fix_symbol s = s +fun repair_bool_literal "true" = "c_True" + | repair_bool_literal "false" = "c_False" +fun repair_name pool "equal" = "c_equal" + | repair_name pool s = ugly_name pool s (* Generalized first-order terms, which include file names, numbers, etc. *) -fun parse_term x = +(* The "x" argument is not strictly necessary, but without it Poly/ML loops + forever at compile time. *) +fun parse_term pool x = (parse_quoted >> atom || parse_integer >> SInt - || $$ "$" |-- Symbol.scan_id >> (atom o fix_bool_literal) - || (Symbol.scan_id >> fix_symbol) - -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> SBranch - || $$ "(" |-- parse_term --| $$ ")" - || $$ "[" |-- Scan.optional parse_terms [] --| $$ "]" >> slist_of) x -and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x + || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal) + || (Symbol.scan_id >> repair_name pool) + -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> SBranch + || $$ "(" |-- parse_term pool --| $$ ")" + || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x +and parse_terms pool x = + (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x fun negate_stree t = SBranch ("c_Not", [t]) fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]); (* Apply equal or not-equal to a term. *) -fun do_equal (t, NONE) = t - | do_equal (t1, SOME (NONE, t2)) = equate_strees t1 t2 - | do_equal (t1, SOME (SOME _, t2)) = negate_stree (equate_strees t1 t2) +fun repair_predicate_term (t, NONE) = t + | repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2 + | repair_predicate_term (t1, SOME (SOME _, t2)) = + negate_stree (equate_strees t1 t2) +fun parse_predicate_term pool = + parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "=" + -- parse_term pool) + >> repair_predicate_term (*Literals can involve negation, = and !=.*) -fun parse_literal x = - ($$ "~" |-- parse_literal >> negate_stree - || (parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) - >> do_equal)) x +fun parse_literal pool x = + ($$ "~" |-- parse_literal pool >> negate_stree || parse_predicate_term pool) x -val parse_literals = parse_literal ::: Scan.repeat ($$ "|" |-- parse_literal) +fun parse_literals pool = + parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool) (*Clause: a list of literals separated by the disjunction sign*) -val parse_clause = - $$ "(" |-- parse_literals --| $$ ")" || Scan.single parse_literal +fun parse_clause pool = + $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool) fun ints_of_stree (SInt n) = cons n | ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts val parse_tstp_annotations = - Scan.optional ($$ "," |-- parse_term --| Scan.option ($$ "," |-- parse_terms) + Scan.optional ($$ "," |-- parse_term NONE + --| Scan.option ($$ "," |-- parse_terms NONE) >> (fn source => ints_of_stree source [])) [] (* ::= cnf(, , ). The could be an identifier, but we assume integers. *) fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps) -val parse_tstp_line = +fun parse_tstp_line pool = (Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ "," - --| Symbol.scan_id --| $$ "," -- parse_clause -- parse_tstp_annotations + --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations --| $$ ")" --| $$ "." >> retuple_tstp_line @@ -127,23 +141,26 @@ (* It is not clear why some literals are followed by sequences of stars. We ignore them. *) -val parse_starred_literal = parse_literal --| Scan.repeat ($$ "*" || $$ " ") +fun parse_starred_predicate_term pool = + parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ") -val parse_horn_clause = - Scan.repeat parse_starred_literal --| $$ "-" --| $$ ">" - -- Scan.repeat parse_starred_literal +fun parse_horn_clause pool = + Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">" + -- Scan.repeat (parse_starred_predicate_term pool) >> (fn ([], []) => [atom "c_False"] | (clauses1, clauses2) => map negate_stree clauses1 @ clauses2) -(* Syntax: [0:] || -> . *) +(* Syntax: [0:] || + -> . *) fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps) -val parse_spass_proof_line = +fun parse_spass_proof_line pool = parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|" - -- parse_horn_clause --| $$ "." + -- parse_horn_clause pool --| $$ "." >> retuple_spass_proof_line -val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line) +fun parse_proof_line pool = + fst o (parse_tstp_line pool || parse_spass_proof_line pool) (**** INTERPRETATION OF TSTP SYNTAX TREES ****) @@ -271,7 +288,7 @@ lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts; (*Update TVars/TFrees with detected sort constraints.*) -fun fix_sorts vt = +fun repair_sorts vt = let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1))) @@ -285,9 +302,10 @@ (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. vt0 holds the initial sort constraints, from the conjecture clauses.*) -fun clause_of_strees ctxt vt0 ts = - let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in - singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt)) +fun clause_of_strees ctxt vt ts = + let val (vt, dt) = lits_of_strees ctxt (vt, []) ts in + dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT + |> Syntax.check_term ctxt end fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t; @@ -491,10 +509,10 @@ fun isar_proof_end 1 = "qed" | isar_proof_end _ = "next" -fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names = +fun isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal i = let val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n") - val tuples = map (parse_proof_line o explode) cnfs + val tuples = map (parse_proof_line pool o explode) cnfs val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n") val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt @@ -600,7 +618,7 @@ val strip_spaces = strip_spaces_in_list o String.explode -fun isar_proof_text debug modulus sorts ctxt +fun isar_proof_text pool debug modulus sorts ctxt (minimize_command, proof, thm_names, goal, i) = let val cnfs = proof |> split_lines |> map strip_spaces |> filter is_proof_line @@ -608,7 +626,8 @@ metis_proof_text (minimize_command, proof, thm_names, goal, i) val tokens = String.tokens (fn c => c = #" ") one_line_proof fun isar_proof_for () = - case isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names of + case isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal + i of "" => "" | isar_proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof @@ -622,8 +641,8 @@ |> the_default "Warning: The Isar proof construction failed.\n" in (one_line_proof ^ isar_proof, lemma_names) end -fun proof_text isar_proof debug modulus sorts ctxt = - if isar_proof then isar_proof_text debug modulus sorts ctxt +fun proof_text isar_proof pool debug modulus sorts ctxt = + if isar_proof then isar_proof_text pool debug modulus sorts ctxt else metis_proof_text end;