# HG changeset patch # User blanchet # Date 1403615299 -7200 # Node ID ff10067b224850c2f165c2adafe3d57fd010a55d # Parent cc2a820320580e34327202e3e9fc5f0da55f2475 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct) diff -r cc2a82032058 -r ff10067b2248 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 24 14:56:08 2014 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 24 15:08:19 2014 +0200 @@ -155,6 +155,8 @@ fun heading_sort_key heading = if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading +val max_dependencies = 100 + fun problem_of_theory ctxt thy format infer_policy type_enc = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt @@ -182,8 +184,8 @@ facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), - th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs) - |> map fact_name_of)) + th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs) + |> these |> map fact_name_of)) val all_problem_names = problem |> maps (map ident_of_problem_line o snd) |> distinct (op =) diff -r cc2a82032058 -r ff10067b2248 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Tue Jun 24 14:56:08 2014 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Tue Jun 24 15:08:19 2014 +0200 @@ -111,7 +111,7 @@ | NONE => error ("No fact called \"" ^ name ^ "\".") val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt - val isar_deps = isar_dependencies_of name_tabs th + val isar_deps = these (isar_dependencies_of name_tabs th) val facts = facts |> filter (fn (_, th') => diff -r cc2a82032058 -r ff10067b2248 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Tue Jun 24 14:56:08 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Tue Jun 24 15:08:19 2014 +0200 @@ -90,6 +90,7 @@ val prover_marker = "$a" val isar_marker = "$i" +val missing_marker = "$m" val omitted_marker = "$o" val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *) val prover_failed_marker = "$x" @@ -105,9 +106,14 @@ let val deps = (case isar_deps_opt of - SOME deps => deps - | NONE => isar_dependencies_of name_tabs th) - in (if null deps then unprovable_marker else isar_marker, deps) end) + NONE => isar_dependencies_of name_tabs th + | deps => deps) + in + ((case deps of + NONE => missing_marker + | SOME [] => unprovable_marker + | SOME deps => isar_marker), []) + end) in (case trim_dependencies deps of SOME deps => (marker, deps) @@ -147,7 +153,7 @@ fun is_bad_query ctxt ho_atp step j th isar_deps = j mod step <> 0 orelse Thm.legacy_get_kind th = "" orelse - null isar_deps orelse + null (the_list isar_deps) orelse is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = @@ -170,7 +176,7 @@ |> sort_wrt fst val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = - smart_dependencies_of ctxt params_opt access_facts name_tabs th (SOME isar_deps) + smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [prop_of th] diff -r cc2a82032058 -r ff10067b2248 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jun 24 14:56:08 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jun 24 15:08:19 2014 +0200 @@ -83,7 +83,7 @@ val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list -> (string * real) list val trim_dependencies : string list -> string list option - val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list + val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> string Symtab.table * string Symtab.table -> thm -> bool * string list val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> @@ -1153,21 +1153,22 @@ if length deps > max_dependencies then NONE else SOME deps fun isar_dependencies_of name_tabs th = - let val deps = thms_in_proof (SOME name_tabs) th in + thms_in_proof max_dependencies (SOME name_tabs) th + |> Option.map (fn deps => if deps = [typedef_dep] orelse deps = [class_some_dep] orelse exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse is_size_def deps th then [] else - deps - end + deps) fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = (case isar_dependencies_of name_tabs th of - [] => (false, []) - | isar_deps => + SOME [] => (false, []) + | isar_deps0 => let + val isar_deps = these isar_deps0 val thy = Proof_Context.theory_of ctxt val goal = goal_of_thm thy th val name = nickname_of_thm th @@ -1533,7 +1534,6 @@ |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) else isar_dependencies_of name_tabs th - |> trim_dependencies fun do_commit [] [] [] state = state | do_commit learns relearns flops {access_G, num_known_facts, dirty} = diff -r cc2a82032058 -r ff10067b2248 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 24 14:56:08 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 24 15:08:19 2014 +0200 @@ -19,7 +19,8 @@ val parse_time : string -> string -> Time.time val subgoal_count : Proof.state -> int val reserved_isar_keyword_table : unit -> unit Symtab.table - val thms_in_proof : (string Symtab.table * string Symtab.table) option -> thm -> string list + val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm -> + string list option val thms_of_name : Proof.context -> string -> thm list val one_day : Time.time val one_year : Time.time @@ -84,11 +85,13 @@ fun reserved_isar_keyword_table () = Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make +exception TOO_MANY of unit + (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to be missing over there; or maybe the two code portions are not doing the same? *) -fun fold_body_thm outer_name (map_plain_name, map_inclass_name) = +fun fold_body_thm max_thms outer_name (map_plain_name, map_inclass_name) body = let - fun app_thm map_name (_, (name, _, body)) accum = + fun app_thm map_name (_, (name, _, body)) (accum as (num_thms, names)) = let val (anonymous, enter_class) = (* The "name = outer_name" case caters for the uncommon case where the proved theorem @@ -98,18 +101,25 @@ else (false, false) in if anonymous then - accum |> app_body (if enter_class then map_inclass_name else map_name) (Future.join body) + app_body (if enter_class then map_inclass_name else map_name) (Future.join body) accum else - accum |> union (op =) (the_list (map_name name)) + (case map_name name of + SOME name' => + if member (op =) names name' then accum + else if num_thms = max_thms then raise TOO_MANY () + else (num_thms + 1, name' :: names) + | NONE => accum) end and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms in - app_body map_plain_name + snd (app_body map_plain_name body (0, [])) end -fun thms_in_proof name_tabs th = +fun thms_in_proof max_thms name_tabs th = let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in - fold_body_thm (Thm.get_name_hint th) map_names (Proofterm.strip_thm (Thm.proof_body_of th)) [] + SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names + (Proofterm.strip_thm (Thm.proof_body_of th))) + handle TOO_MANY () => NONE end fun thms_of_name ctxt name =