# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 82d6e46c673f79071bd7124c5bca77edb27fb178 # Parent ee33ba3c0e053bead7886df9de39d389acb5efab fixed order of accessibles + other tweaks to MaSh diff -r ee33ba3c0e05 -r 82d6e46c673f src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -107,15 +107,21 @@ handle TYPE _ => @{prop True} end +fun all_non_tautological_facts_of thy css_table = + Sledgehammer_Fact.all_facts_of thy css_table + |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology orf + Sledgehammer_Filter_MaSh.is_too_meta) o snd) + fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val type_enc = type_enc |> type_enc_from_string Strict - |> adjust_type_enc format + val type_enc = + type_enc |> type_enc_from_string Strict + |> adjust_type_enc format val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = Sledgehammer_Fact.all_facts_of thy css_table + val facts = all_non_tautological_facts_of thy css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r ee33ba3c0e05 -r 82d6e46c673f src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -16,9 +16,10 @@ structure MaSh_Eval : MASH_EVAL = struct +open Sledgehammer_Fact open Sledgehammer_Filter_MaSh -val isarN = "Isa" +val isarN = "Isar" val iterN = "Iter" val mashN = "MaSh" val meshN = "Mesh" @@ -34,8 +35,11 @@ val path = file_name |> Path.explode val lines = path |> File.read_lines val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_non_tautological_facts_of thy css_table - val all_names = facts |> map (Thm.get_name_hint o snd) + val facts = all_facts_of thy css_table + val all_names = + facts |> map snd + |> filter_out (is_likely_tautology orf is_too_meta) + |> map Thm.get_name_hint val iter_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 val mesh_ok = Unsynchronized.ref 0 diff -r ee33ba3c0e05 -r 82d6e46c673f src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -37,16 +37,16 @@ val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" val _ = File.append path s in [fact] end - val thy_facts = - all_non_tautological_facts_of thy Termtab.empty + val thy_map = + all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) - |> thy_facts_from_thms + |> thy_map_from_facts fun do_thy facts = let val thy = thy_of_fact thy (hd facts) - val parents = parent_facts thy thy_facts + val parents = parent_facts thy thy_map in fold do_fact facts parents; () end - in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end + in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end fun generate_features ctxt thy include_thy file_name = let @@ -54,7 +54,7 @@ val _ = File.write path "" val css_table = clasimpset_rule_table_of ctxt val facts = - all_non_tautological_facts_of thy css_table + all_facts_of thy css_table |> not include_thy ? filter_out (has_thy thy o snd) fun do_fact ((_, (_, status)), th) = let @@ -69,10 +69,12 @@ val path = file_name |> Path.explode val _ = File.write path "" val ths = - all_non_tautological_facts_of thy Termtab.empty + all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd - val all_names = ths |> map Thm.get_name_hint + val all_names = + ths |> filter_out (is_likely_tautology orf is_too_meta) + |> map Thm.get_name_hint fun do_thm th = let val name = Thm.get_name_hint th @@ -87,10 +89,12 @@ val path = file_name |> Path.explode val _ = File.write path "" val facts = - all_non_tautological_facts_of thy Termtab.empty + all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint + val all_names = + ths |> filter_out (is_likely_tautology orf is_too_meta) + |> map Thm.get_name_hint fun is_dep dep (_, th) = Thm.get_name_hint th = dep fun add_isa_dep facts dep accum = if exists (is_dep dep) accum then @@ -133,12 +137,14 @@ val path = file_name |> Path.explode val _ = File.write path "" val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_non_tautological_facts_of thy css_table + val facts = all_facts_of thy css_table val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint + val all_names = + ths |> filter_out (is_likely_tautology orf is_too_meta) + |> map Thm.get_name_hint fun do_fact ((_, (_, status)), th) prevs = let val name = Thm.get_name_hint th @@ -152,8 +158,8 @@ escape_metas deps ^ "\n" val _ = File.append path (query ^ update) in [name] end - val thy_facts = old_facts |> thy_facts_from_thms - val parents = parent_facts thy thy_facts + val thy_map = old_facts |> thy_map_from_facts + val parents = parent_facts thy thy_map in fold do_fact new_facts parents; () end fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant @@ -162,7 +168,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_non_tautological_facts_of thy css_table + val facts = all_facts_of thy css_table val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) diff -r ee33ba3c0e05 -r 82d6e46c673f src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,13 +26,13 @@ val extract_query : string -> string * string list val suggested_facts : string list -> fact list -> fact list val mesh_facts : int -> (fact list * int option) list -> fact list - val all_non_tautological_facts_of : - theory -> status Termtab.table -> fact list + val is_likely_tautology : thm -> bool + val is_too_meta : thm -> bool val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order - val thy_facts_from_thms : fact list -> string list Symtab.table + val thy_map_from_facts : fact list -> (string * string list) list val has_thy : theory -> thm -> bool - val parent_facts : theory -> string list Symtab.table -> string list + val parent_facts : theory -> (string * string list) list -> string list val features_of : theory -> status -> term list -> string list val isabelle_dependencies_of : string list -> thm -> string list val goal_of_thm : theory -> thm -> thm @@ -49,7 +49,6 @@ val mash_suggest_facts : Proof.context -> params -> string -> term list -> term -> fact list -> fact list - val mash_can_learn_thy : Proof.context -> theory -> bool val mash_learn_thy : Proof.context -> theory -> real -> unit val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit val relevant_facts : @@ -103,14 +102,13 @@ val escape_meta = String.translate meta_char val escape_metas = map escape_meta #> space_implode " " -val unescape_meta = unmeta_chars [] o String.explode -val unescape_metas = map unescape_meta o space_explode " " +val unescape_meta = String.explode #> unmeta_chars [] +val unescape_metas = + space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta -val explode_suggs = - space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta fun extract_query line = case space_explode ":" line of - [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs) + [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) | _ => ("", []) fun find_suggested facts sugg = @@ -230,37 +228,37 @@ null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) -fun is_too_meta thy th = - fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} - -fun all_non_tautological_facts_of thy css_table = - all_facts_of thy css_table - |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) +(* ### FIXME: optimize *) +fun is_too_meta th = + fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th)) + <> @{typ bool} fun theory_ord p = - if Theory.eq_thy p then EQUAL - else if Theory.subthy p then LESS - else if Theory.subthy (swap p) then GREATER - else EQUAL + if Theory.eq_thy p then + EQUAL + else if Theory.subthy p then + LESS + else if Theory.subthy (swap p) then + GREATER + else case int_ord (pairself (length o Theory.ancestors_of) p) of + EQUAL => string_ord (pairself Context.theory_name p) + | order => order val thm_ord = theory_ord o pairself theory_of_thm -(* ### FIXME: optimize *) -fun thy_facts_from_thms ths = - ths |> map (snd #> `(theory_of_thm #> Context.theory_name)) - |> AList.group (op =) - |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm - o hd o snd)) - |> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint)) - |> Symtab.make +fun thy_map_from_facts ths = + ths |> sort (thm_ord o swap o pairself snd) + |> map (snd #> `(theory_of_thm #> Context.theory_name)) + |> AList.coalesce (op =) + |> map (apsnd (map Thm.get_name_hint)) fun has_thy thy th = Context.theory_name thy = Context.theory_name (theory_of_thm th) -fun parent_facts thy thy_facts = +fun parent_facts thy thy_map = let fun add_last thy = - case Symtab.lookup thy_facts (Context.theory_name thy) of + case AList.lookup (op =) thy_map (Context.theory_name thy) of SOME (last_fact :: _) => insert (op =) last_fact | _ => add_parent thy and add_parent thy = fold add_last (Theory.parents_of thy) @@ -312,10 +310,10 @@ Sledgehammer_Provers.Normal (hd provers) in prover params (K (K (K ""))) problem end -fun accessibility_of thy thy_facts = - case Symtab.lookup thy_facts (Context.theory_name thy) of +fun accessibility_of thy thy_map = + case AList.lookup (op =) thy_map (Context.theory_name thy) of SOME (fact :: _) => [fact] - | _ => parent_facts thy thy_facts + | _ => parent_facts thy thy_map val thy_name_of_fact = hd o Long_Name.explode @@ -376,12 +374,10 @@ (*** High-level communication with MaSh ***) type mash_state = - {dirty_thys : unit Symtab.table, - thy_facts : string list Symtab.table} + {dirty_thys : string list, + thy_map : (string * string list) list} -val empty_state = - {dirty_thys = Symtab.empty, - thy_facts = Symtab.empty} +val empty_state = {dirty_thys = [], thy_map = []} local @@ -392,28 +388,25 @@ case try File.read_lines path of SOME (dirty_line :: facts_lines) => let - fun dirty_thys_of_line line = - Symtab.make (line |> unescape_metas |> map (rpair ())) fun add_facts_line line = case unescape_metas line of - thy :: facts => Symtab.update_new (thy, facts) + thy :: facts => cons (thy, facts) | _ => I (* shouldn't happen *) in - {dirty_thys = dirty_thys_of_line dirty_line, - thy_facts = fold add_facts_line facts_lines Symtab.empty} + {dirty_thys = unescape_metas dirty_line, + thy_map = fold_rev add_facts_line facts_lines []} end | _ => empty_state) end -fun mash_save ({dirty_thys, thy_facts} : mash_state) = +fun mash_save ({dirty_thys, thy_map} : mash_state) = let val path = mash_state_path () - val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n" + val dirty_line = escape_metas dirty_thys ^ "\n" fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" in File.write path dirty_line; - Symtab.fold (fn thy_fact => fn () => - File.append path (fact_line_for thy_fact)) thy_facts () + List.app (File.append path o fact_line_for) thy_map end val global_state = @@ -434,22 +427,19 @@ end fun mash_can_suggest_facts (_ : Proof.context) = - not (Symtab.is_empty (#thy_facts (mash_get ()))) + mash_home () <> "" andalso not (null (#thy_map (mash_get ()))) fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt - val thy_facts = #thy_facts (mash_get ()) - val access = accessibility_of thy thy_facts + val thy_map = #thy_map (mash_get ()) + val access = accessibility_of thy thy_map val feats = features_of thy General (concl_t :: hyp_ts) val suggs = mash_QUERY ctxt (access, feats) in suggested_facts suggs facts end -fun mash_can_learn_thy (_ : Proof.context) thy = - not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy)) - -fun is_fact_in_thy_facts thy_facts fact = - case Symtab.lookup thy_facts (thy_name_of_fact fact) of +fun is_fact_in_thy_map thy_map fact = + case AList.lookup (op =) thy_map (thy_name_of_fact fact) of SOME facts => member (op =) facts fact | NONE => false @@ -465,20 +455,22 @@ else new :: old :: zip_facts news olds -fun add_thy_facts_from_thys new old = - let - fun add_thy (thy, new_facts) = - case Symtab.lookup old thy of - SOME old_facts => Symtab.update (thy, zip_facts old_facts new_facts) - | NONE => Symtab.update_new (thy, new_facts) - in old |> Symtab.fold add_thy new end +fun add_thy_map_from_thys [] old = old + | add_thy_map_from_thys new old = + let + fun add_thy (thy, new_facts) = + case AList.lookup (op =) old thy of + SOME old_facts => + AList.update (op =) (thy, zip_facts old_facts new_facts) + | NONE => cons (thy, new_facts) + in old |> fold add_thy new end fun mash_learn_thy ctxt thy timeout = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_non_tautological_facts_of thy css_table - val {thy_facts, ...} = mash_get () - fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th) + val facts = all_facts_of thy css_table + val {thy_map, ...} = mash_get () + fun is_old (_, th) = is_fact_in_thy_map thy_map (Thm.get_name_hint th) val (old_facts, new_facts) = facts |> List.partition is_old ||> sort (thm_ord o pairself snd) in @@ -487,7 +479,9 @@ else let val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint + val all_names = + ths |> filter_out (is_likely_tautology orf is_too_meta) + |> map Thm.get_name_hint fun do_fact ((_, (_, status)), th) (prevs, upds) = let val name = Thm.get_name_hint th @@ -495,27 +489,27 @@ val deps = isabelle_dependencies_of all_names th val upd = (name, prevs, feats, deps) in ([name], upd :: upds) end - val parents = parent_facts thy thy_facts + val parents = parent_facts thy thy_map val (_, upds) = (parents, []) |> fold do_fact new_facts - val new_thy_facts = new_facts |> thy_facts_from_thms - fun trans {dirty_thys, thy_facts} = + val new_thy_map = new_facts |> thy_map_from_facts + fun trans {dirty_thys, thy_map} = (mash_ADD ctxt (rev upds); {dirty_thys = dirty_thys, - thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts}) + thy_map = thy_map |> add_thy_map_from_thys new_thy_map}) in mash_map trans end end fun mash_learn_proof ctxt thy t ths = - mash_map (fn state as {dirty_thys, thy_facts} => + mash_map (fn state as {dirty_thys, thy_map} => let val deps = ths |> map Thm.get_name_hint in - if forall (is_fact_in_thy_facts thy_facts) deps then + if forall (is_fact_in_thy_map thy_map) deps then let val fact = ATP_Util.timestamp () (* should be fairly fresh *) - val access = accessibility_of thy thy_facts + val access = accessibility_of thy thy_map val feats = features_of thy General [t] in mash_ADD ctxt [(fact, access, feats, deps)]; - {dirty_thys = dirty_thys, thy_facts = thy_facts} + {dirty_thys = dirty_thys, thy_map = thy_map} end else state @@ -534,7 +528,7 @@ val fact_filter = case fact_filter of SOME ff => ff - | NONE => if mash_home () = "" then iterN else meshN + | NONE => if mash_can_suggest_facts ctxt then meshN else iterN val add_ths = Attrib.eval_thms ctxt add fun prepend_facts ths accepts = ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @