# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 50e64af9c8290391351fbebbfd5858b01ec8756f # Parent f1d135d0ea69d1b1c9e6aebd9494c3df9bf22bdb more work on MaSh diff -r f1d135d0ea69 -r 50e64af9c829 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:04 2012 +0200 @@ -14,7 +14,6 @@ lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] ML {* -open Sledgehammer_Filter_MaSh open MaSh_Export *} @@ -26,7 +25,7 @@ ML {* if do_it then - generate_accessibility @{context} thy false "/tmp/mash_accessibility" + generate_accessibility thy false "/tmp/mash_accessibility" else () *} @@ -40,7 +39,7 @@ ML {* if do_it then - generate_isa_dependencies @{context} thy false "/tmp/mash_isa_dependencies" + generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" else () *} diff -r f1d135d0ea69 -r 50e64af9c829 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 @@ -9,6 +9,11 @@ sig type params = Sledgehammer_Provers.params + val generate_accessibility : theory -> bool -> string -> unit + val generate_features : Proof.context -> theory -> bool -> string -> unit + val generate_isa_dependencies : theory -> bool -> string -> unit + val generate_atp_dependencies : + Proof.context -> params -> theory -> bool -> string -> unit val generate_commands : Proof.context -> theory -> string -> unit val generate_iter_suggestions : Proof.context -> params -> theory -> int -> string -> unit @@ -17,8 +22,112 @@ structure MaSh_Export : MASH_EXPORT = struct +open Sledgehammer_Fact +open Sledgehammer_Filter_Iter open Sledgehammer_Filter_MaSh +fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact + +fun generate_accessibility thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + fun do_fact fact prevs = + let + 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 + |> not include_thy ? filter_out (has_thy thy o snd) + |> thy_facts_from_thms + fun do_thy facts = + let + val thy = thy_of_fact thy (hd facts) + val parents = parent_facts thy thy_facts + in fold do_fact facts parents; () end + in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end + +fun generate_features ctxt thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val css_table = clasimpset_rule_table_of ctxt + val facts = + all_non_tautological_facts_of thy css_table + |> not include_thy ? filter_out (has_thy thy o snd) + fun do_fact ((_, (_, status)), th) = + let + val name = Thm.get_name_hint th + val feats = features_of (theory_of_thm th) status [prop_of th] + val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" + in File.append path s end + in List.app do_fact facts end + +fun generate_isa_dependencies thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val ths = + all_non_tautological_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 + fun do_thm th = + let + val name = Thm.get_name_hint th + val deps = isabelle_dependencies_of all_names th + val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" + in File.append path s end + in List.app do_thm ths end + +fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy + include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = + all_non_tautological_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 + 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 + accum + else case find_first (is_dep dep) facts of + SOME ((name, status), th) => accum @ [((name, status), th)] + | NONE => accum (* shouldn't happen *) + fun fix_name ((_, stature), th) = + ((fn () => th |> Thm.get_name_hint, stature), th) + fun do_thm th = + let + val name = Thm.get_name_hint th + val goal = goal_of_thm thy th + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 + val deps = + case isabelle_dependencies_of all_names th of + [] => [] + | isa_dep as [_] => isa_dep (* can hardly beat that *) + | isa_deps => + let + val facts = + facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val facts = + facts |> iterative_relevant_facts ctxt params (hd provers) + (the max_facts) NONE hyp_ts concl_t + |> fold (add_isa_dep facts) isa_deps + |> map fix_name + in + case run_prover ctxt params facts goal of + {outcome = NONE, used_facts, ...} => + used_facts |> map fst |> sort string_ord + | _ => isa_deps + end + val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" + in File.append path s end + in List.app do_thm ths end + fun generate_commands ctxt thy file_name = let val path = file_name |> Path.explode @@ -36,12 +145,11 @@ val feats = features_of thy status [prop_of th] val deps = isabelle_dependencies_of all_names th val kind = Thm.legacy_get_kind th - val core = - space_implode " " prevs ^ "; " ^ space_implode " " feats + val core = escape_metas prevs ^ "; " ^ escape_metas feats val query = if kind <> "" then "? " ^ core ^ "\n" else "" val update = "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ - space_implode " " deps ^ "\n" + escape_metas deps ^ "\n" val _ = File.append path (query ^ update) in [name] end val thy_facts = old_facts |> thy_facts_from_thms diff -r f1d135d0ea69 -r 50e64af9c829 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 @@ -27,14 +27,9 @@ val isabelle_dependencies_of : string list -> thm -> string list val goal_of_thm : theory -> thm -> thm val run_prover : Proof.context -> params -> fact list -> thm -> prover_result - val generate_accessibility : Proof.context -> theory -> bool -> string -> unit - val generate_features : Proof.context -> theory -> bool -> string -> unit - val generate_isa_dependencies : - Proof.context -> theory -> bool -> string -> unit - val generate_atp_dependencies : - Proof.context -> params -> theory -> bool -> string -> unit + val thy_name_of_fact : string -> string val mash_RESET : unit -> unit - val mash_ADD : string -> string list -> string list -> string list -> unit + val mash_ADD : (string * string list * string list * string list) list -> unit val mash_DEL : string list -> string list -> unit val mash_SUGGEST : string list -> string list -> string list val mash_reset : unit -> unit @@ -43,7 +38,7 @@ Proof.context -> params -> string -> int -> term list -> term -> fact list -> fact list * fact list val mash_can_learn_thy : theory -> bool - val mash_learn_thy : theory -> real -> unit + val mash_learn_thy : Proof.context -> real -> unit val mash_learn_proof : theory -> term -> thm list -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list @@ -138,11 +133,13 @@ let val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] val bad_consts = atp_widely_irrelevant_consts + fun add_classes @{sort type} = I + | add_classes S = union (op =) (map class_name_of S) fun do_add_type (Type (s, Ts)) = (not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) #> fold do_add_type Ts - | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S) - | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S) + | do_add_type (TFree (_, S)) = add_classes S + | do_add_type (TVar (_, S)) = add_classes S fun add_type T = type_max_depth >= 0 ? do_add_type T fun mk_app s args = if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" @@ -265,7 +262,7 @@ let val thy = theory_of_thm (hd facts) val parents = parent_facts thy_facts thy - in add_thms facts parents end + in add_facts facts parents end in fold (add_thy o snd) thy_facts end *) @@ -274,117 +271,22 @@ SOME (fact :: _) => [fact] | _ => parent_facts thy thy_facts -fun theory_of_fact thy fact = - Context.this_theory thy (hd (Long_Name.explode fact)) - -fun generate_accessibility ctxt thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - fun do_fact fact prevs = - let - 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 - |> not include_thy ? filter_out (has_thy thy o snd) - |> thy_facts_from_thms - fun do_thy facts = - let - val thy = theory_of_fact thy (hd facts) - val parents = parent_facts thy thy_facts - in fold do_fact facts parents; () end - in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end - -fun generate_features ctxt thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val css_table = clasimpset_rule_table_of ctxt - val facts = - all_non_tautological_facts_of thy css_table - |> not include_thy ? filter_out (has_thy thy o snd) - fun do_fact ((_, (_, status)), th) = - let - val name = Thm.get_name_hint th - val feats = features_of (theory_of_thm th) status [prop_of th] - val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" - in File.append path s end - in List.app do_fact facts end - -fun generate_isa_dependencies ctxt thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val ths = - all_non_tautological_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 - fun do_thm th = - let - val name = Thm.get_name_hint th - val deps = isabelle_dependencies_of all_names th - val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" - in File.append path s end - in List.app do_thm ths end - -fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy - include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val facts = - all_non_tautological_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 - 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 - accum - else case find_first (is_dep dep) facts of - SOME ((name, status), th) => accum @ [((name, status), th)] - | NONE => accum (* shouldn't happen *) - fun fix_name ((_, stature), th) = - ((fn () => th |> Thm.get_name_hint, stature), th) - fun do_thm th = - let - val name = Thm.get_name_hint th - val goal = goal_of_thm thy th - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 - val deps = - case isabelle_dependencies_of all_names th of - [] => [] - | isa_dep as [_] => isa_dep (* can hardly beat that *) - | isa_deps => - let - val facts = - facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val facts = - facts |> iterative_relevant_facts ctxt params (hd provers) - (the max_facts) NONE hyp_ts concl_t - |> fold (add_isa_dep facts) isa_deps - |> map fix_name - in - case run_prover ctxt params facts goal of - {outcome = NONE, used_facts, ...} => - used_facts |> map fst |> sort string_ord - | _ => isa_deps - end - val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" - in File.append path s end - in List.app do_thm ths end +val thy_name_of_fact = hd o Long_Name.explode (*** Low-level communication with MaSh ***) fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file)) -fun mash_ADD fact access feats deps = - warning ("MaSh ADD " ^ fact ^ ": " ^ escape_metas access ^ "; " ^ - escape_metas feats ^ "; " ^ escape_metas deps) +val mash_ADD = + let + fun add_fact (fact, access, feats, deps) = + let + val s = + escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ + escape_metas feats ^ "; " ^ escape_metas deps + in warning ("MaSh ADD " ^ s) end + in List.app add_fact end fun mash_DEL facts feats = warning ("MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) @@ -401,7 +303,7 @@ completed_thys : unit Symtab.table, thy_facts : string list Symtab.table} -val mash_zero = +val empty_state = {fresh = 0, completed_thys = Symtab.empty, thy_facts = Symtab.empty} @@ -429,7 +331,7 @@ completed_thys = comp_thys_of_line comp_line, thy_facts = fold add_facts_line facts_lines Symtab.empty} end - | _ => mash_zero) + | _ => empty_state) end fun mash_save ({fresh, completed_thys, thy_facts} : mash_state) = @@ -444,52 +346,100 @@ end val global_state = - Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, mash_zero) + Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state) in +fun mash_set state = + Synchronized.change global_state (K (true, state |> tap mash_save)) + fun mash_change f = Synchronized.change global_state (mash_load ##> (f #> tap mash_save)) fun mash_peek f = Synchronized.change global_state (mash_load ##> tap f) -fun mash_value () = Synchronized.change_result global_state (mash_load #> `snd) +fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd) fun mash_reset () = Synchronized.change global_state (fn _ => - (mash_RESET (); File.rm (mk_path state_file); (true, mash_zero))) + (mash_RESET (); File.rm (mk_path state_file); (true, empty_state))) end -fun mash_can_suggest_facts () = - not (Symtab.is_empty (#thy_facts (mash_value ()))) +fun mash_can_suggest_facts () = not (Symtab.is_empty (#thy_facts (mash_get ()))) fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt - val access = accessibility_of thy (#thy_facts (mash_value ())) + val access = accessibility_of thy (#thy_facts (mash_get ())) val feats = features_of thy General (concl_t :: hyp_ts) val suggs = mash_SUGGEST access feats in (facts, []) end fun mash_can_learn_thy thy = - not (Symtab.defined (#completed_thys (mash_value ())) - (Context.theory_name thy)) + not (Symtab.defined (#completed_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 + SOME facts => member (op =) facts fact + | NONE => false -fun mash_learn_thy thy timeout = () -(* ### *) +fun mash_learn_thy ctxt timeout = + let + val thy = Proof_Context.theory_of ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = all_non_tautological_facts_of thy css_table + val {fresh, completed_thys, thy_facts} = mash_get () + fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th) + val (old_facts, new_facts) = + facts |> List.partition is_old ||> sort (thm_ord o pairself snd) + val ths = facts |> map snd + val all_names = ths |> map Thm.get_name_hint + fun do_fact ((_, (_, status)), th) prevs = + let + val name = Thm.get_name_hint th + val feats = features_of thy status [prop_of th] + val deps = isabelle_dependencies_of all_names th + val kind = Thm.legacy_get_kind th + val s = + "! " ^ escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ + escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" + in [name] end + val thy_facts = old_facts |> thy_facts_from_thms + val parents = parent_facts thy thy_facts + in + fold do_fact new_facts parents; + mash_set {fresh = fresh, completed_thys = completed_thys, + thy_facts = thy_facts} + end + +(* ### +fun compute_accessibility thy thy_facts = + let + fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th] + fun add_thy facts = + let + val thy = theory_of_thm (hd facts) + val parents = parent_facts thy_facts thy + in add_facts facts parents end + in fold (add_thy o snd) thy_facts end +*) fun mash_learn_proof thy t ths = - mash_change (fn {fresh, completed_thys, thy_facts} => - let - val fact = fresh_fact_prefix ^ string_of_int fresh - val access = accessibility_of thy thy_facts - val feats = features_of thy General [t] - val deps = ths |> map Thm.get_name_hint - in - mash_ADD fact access feats deps; - {fresh = fresh + 1, completed_thys = completed_thys, - thy_facts = thy_facts} + mash_change (fn state as {fresh, completed_thys, thy_facts} => + let val deps = ths |> map Thm.get_name_hint in + if forall (is_fact_in_thy_facts thy_facts) deps then + let + val fact = fresh_fact_prefix ^ string_of_int fresh + val access = accessibility_of thy thy_facts + val feats = features_of thy General [t] + in + mash_ADD [(fact, access, feats, deps)]; + {fresh = fresh + 1, completed_thys = completed_thys, + thy_facts = thy_facts} + end + else + state end) fun relevant_facts ctxt params prover max_facts