# HG changeset patch # User blanchet # Date 1305888479 -7200 # Node ID dbdfe2d5b6ab6c2c6c1d453fe994ddef96377eec # Parent 221af561ebf9c23cab531a537ada5bec90f30ccb automatically use "metisFT" when typed helpers are necessary diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri May 20 12:47:59 2011 +0200 @@ -14,7 +14,7 @@ type minimize_command = string list -> string type metis_params = string * minimize_command * type_system * string proof * int - * (string * locality) list vector * thm * int + * (string * locality) list vector * int list * thm * int type isar_params = Proof.context * bool * int * string Symtab.table * int list list * int Symtab.table @@ -22,8 +22,8 @@ val repair_conjecture_shape_and_fact_names : type_system -> string -> int list list -> int - -> (string * locality) list vector - -> int list list * int * (string * locality) list vector + -> (string * locality) list vector -> int list + -> int list list * int * (string * locality) list vector * int list val used_facts_in_atp_proof : type_system -> int -> (string * locality) list vector -> string proof -> (string * locality) list @@ -55,7 +55,7 @@ type minimize_command = string list -> string type metis_params = string * minimize_command * type_system * string proof * int - * (string * locality) list vector * thm * int + * (string * locality) list vector * int list * thm * int type isar_params = Proof.context * bool * int * string Symtab.table * int list list * int Symtab.table @@ -64,6 +64,9 @@ 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 + fun find_first_in_list_vector vec key = Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key | (_, value) => value) NONE vec @@ -102,7 +105,7 @@ ? (space_implode "_" o tl o space_explode "_") fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape - fact_offset fact_names = + fact_offset fact_names typed_helpers = if String.isSubstring set_ClauseFormulaRelationN output then let val j0 = hd (hd conjecture_shape) @@ -122,13 +125,17 @@ error ("No such fact: " ^ quote name ^ ".")) in (conjecture_shape |> map (maps renumber_conjecture), 0, - seq |> map names_for_number |> Vector.fromList) + 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) + (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 type_sys _ fact_names (_, SOME s) = (case try (unprefix fact_prefix) s of SOME s' => @@ -139,15 +146,18 @@ end | NONE => []) | resolve_fact _ facts_offset fact_names (num, NONE) = - case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of - SOME j => - let val j = j - facts_offset in - if j > 0 andalso j <= Vector.length fact_names then - Vector.sub (fact_names, j - 1) - else - [] - end - | NONE => [] + (case extract_step_number num of + SOME j => + let val j = j - facts_offset in + if j > 0 andalso j <= Vector.length fact_names then + Vector.sub (fact_names, j - 1) + else + [] + end + | NONE => []) + +fun is_fact type_sys conjecture_shape = + not o null o resolve_fact type_sys 0 conjecture_shape fun resolve_conjecture _ (_, SOME s) = (case try (unprefix conjecture_prefix) s of @@ -157,18 +167,21 @@ | NONE => []) | NONE => []) | resolve_conjecture conjecture_shape (num, NONE) = - case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of - SOME i => - (case find_index (exists (curry (op =) i)) conjecture_shape of - ~1 => [] - | j => [j]) + case extract_step_number num of + SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of + ~1 => [] + | j => [j]) | NONE => [] -fun is_fact type_sys conjecture_shape = - not o null o resolve_fact type_sys 0 conjecture_shape fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape +fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s + | is_typed_helper typed_helpers (num, NONE) = + (case extract_step_number num of + SOME i => member (op =) typed_helpers i + | NONE => false) + fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) = append (resolve_fact type_sys facts_offset fact_names name) | add_fact _ _ _ _ = I @@ -227,15 +240,21 @@ List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) +fun uses_typed_helpers typed_helpers = + exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name + | _ => false) + fun metis_proof_text (banner, minimize_command, type_sys, atp_proof, - facts_offset, fact_names, goal, i) = + facts_offset, fact_names, typed_helpers, goal, i) = let val (chained, extra) = atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names |> split_used_facts + val full_types = uses_typed_helpers typed_helpers atp_proof val n = Logic.count_prems (prop_of goal) + val metis = metis_command full_types i n ([], map fst extra) in - (try_command_line banner (metis_command false i n ([], map fst extra)) ^ + (try_command_line banner metis ^ minimize_line minimize_command (map fst (extra @ chained)), extra @ chained) end @@ -919,7 +938,7 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end -fun string_for_proof ctxt0 i n = +fun string_for_proof ctxt0 full_types i n = let val ctxt = ctxt0 |> Config.put show_free_types false @@ -942,7 +961,7 @@ if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) fun do_facts (ls, ss) = - metis_command false 1 1 + metis_command full_types 1 1 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) and do_step ind (Fix xs) = @@ -979,11 +998,12 @@ fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) (metis_params as (_, _, type_sys, atp_proof, facts_offset, - fact_names, goal, i)) = + fact_names, typed_helpers, goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] + val full_types = uses_typed_helpers typed_helpers atp_proof val n = Logic.count_prems (prop_of goal) val (one_line_proof, lemma_names) = metis_proof_text metis_params fun isar_proof_for () = @@ -995,7 +1015,7 @@ |> then_chain_proof |> kill_useless_labels_in_proof |> relabel_proof - |> string_for_proof ctxt i n of + |> string_for_proof ctxt full_types i n of "" => "\nNo structured proof available (proof too short)." | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof val isar_proof = diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200 @@ -28,6 +28,8 @@ val readable_names : bool Config.T val fact_prefix : string val conjecture_prefix : string + val helper_prefix : string + val typed_helper_suffix : string val predicator_base : string val explicit_app_base : string val type_pred_base : string @@ -46,7 +48,7 @@ -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list -> string problem * string Symtab.table * int * int - * (string * 'a) list vector * int Symtab.table + * (string * 'a) list vector * int list * int Symtab.table val atp_problem_weights : string problem -> (string * real) list end; @@ -87,6 +89,9 @@ val arity_clause_prefix = "arity_" val tfree_prefix = "tfree_" +val typed_helper_suffix = "_T" +val untyped_helper_suffix = "_U" + val predicator_base = "hBOOL" val explicit_app_base = "hAPP" val type_pred_base = "is" @@ -487,7 +492,7 @@ if prem_kind = Conjecture then update_combformula mk_anot else I) in - make_formula ctxt true true (string_of_int j) Chained kind t + make_formula ctxt true true (string_of_int j) General kind t |> maybe_negate end) (0 upto last) ts @@ -734,8 +739,10 @@ val thy = Proof_Context.theory_of ctxt val unmangled_s = mangled_s |> unmangled_const_name fun dub_and_inst c needs_some_types (th, j) = - ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""), - Chained), + ((c ^ "_" ^ string_of_int j ^ + (if needs_some_types then typed_helper_suffix + else untyped_helper_suffix), + General), let val t = th |> prop_of in t |> ((case general_type_arg_policy type_sys of Mangled_Type_Args _ => true @@ -1203,6 +1210,10 @@ (conjs, helpers @ facts) |> sym_decl_table_for_facts type_sys repaired_sym_tab |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys + val helper_lines = + map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys) + (0 upto length helpers - 1 ~~ helpers) + |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ()) (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = @@ -1211,11 +1222,7 @@ (0 upto length facts - 1 ~~ facts)), (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), (aritiesN, map formula_line_for_arity_clause arity_clauses), - (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts - type_sys) - (0 upto length helpers - 1 ~~ helpers) - |> should_add_ti_ti_helper type_sys - ? cons (ti_ti_helper_fact ())), + (helpersN, helper_lines), (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys) conjs), (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))] @@ -1228,6 +1235,13 @@ | _ => I) val (problem, pool) = problem |> nice_atp_problem (Config.get ctxt readable_names) + val helpers_offset = offset_of_heading_in_problem helpersN problem 0 + val typed_helpers = + map_filter (fn (j, {name, ...}) => + if String.isSuffix typed_helper_suffix name then SOME j + else NONE) + ((helpers_offset + 1 upto helpers_offset + length helpers) + ~~ helpers) fun add_sym_arity (s, {min_ary, ...} : sym_info) = if min_ary > 0 then case strip_prefix_and_unascii const_prefix s of @@ -1241,6 +1255,7 @@ offset_of_heading_in_problem conjsN problem 0, offset_of_heading_in_problem factsN problem 0, fact_names |> Vector.fromList, + typed_helpers, Symtab.empty |> Symtab.fold add_sym_arity sym_tab) end diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 20 12:47:59 2011 +0200 @@ -534,7 +534,7 @@ else () val (atp_problem, pool, conjecture_offset, facts_offset, - fact_names, sym_tab) = + fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem @@ -567,13 +567,14 @@ extract_tstplike_proof_and_outcome verbose complete res_code proof_delims known_failures output |>> atp_proof_from_tstplike_proof - val (conjecture_shape, facts_offset, fact_names) = + val (conjecture_shape, facts_offset, fact_names, + typed_helpers) = if is_none outcome then repair_conjecture_shape_and_fact_names type_sys output - conjecture_shape facts_offset fact_names + conjecture_shape facts_offset fact_names typed_helpers else (* don't bother repairing *) - (conjecture_shape, facts_offset, fact_names) + (conjecture_shape, facts_offset, fact_names, typed_helpers) val outcome = case outcome of NONE => @@ -587,7 +588,8 @@ else SOME IncompleteUnprovable | _ => outcome in - ((pool, conjecture_shape, facts_offset, fact_names, sym_tab), + ((pool, conjecture_shape, facts_offset, fact_names, + typed_helpers, sym_tab), (output, msecs, type_sys, atp_proof, outcome)) end val timer = Timer.startRealTimer () @@ -607,7 +609,7 @@ end | maybe_run_slice _ _ result = result fun maybe_blacklist_facts_and_retry iter blacklist - (result as ((_, _, facts_offset, fact_names, _), + (result as ((_, _, facts_offset, fact_names, _, _), (_, _, type_sys, atp_proof, SOME (UnsoundProof (false, _))))) = (case used_facts_in_atp_proof type_sys facts_offset fact_names @@ -624,7 +626,7 @@ result) | maybe_blacklist_facts_and_retry _ _ result = result in - ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty), + ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty), ("", SOME 0, hd fallback_best_type_systems, [], SOME InternalError)) |> fold (maybe_run_slice []) actual_slices @@ -644,7 +646,8 @@ () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output - val ((pool, conjecture_shape, facts_offset, fact_names, sym_tab), + val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers, + sym_tab), (output, msecs, type_sys, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = @@ -668,7 +671,7 @@ (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) val metis_params = (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset, - fact_names, goal, subgoal) + fact_names, typed_helpers, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE => diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Fri May 20 12:47:58 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Fri May 20 12:47:59 2011 +0200 @@ -103,7 +103,7 @@ else Sledgehammer_ATP_Translate.Const_Arg_Types, Sledgehammer_ATP_Translate.Heavy) val explicit_apply = false - val (atp_problem, _, _, _, _, _) = + val (atp_problem, _, _, _, _, _, _) = Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts val infers =