blanchet@49249: (* Title: HOL/TPTP/mash_export.ML blanchet@49249: Author: Jasmin Blanchette, TU Muenchen blanchet@49249: Copyright 2012 blanchet@49249: blanchet@49249: Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). blanchet@49249: *) blanchet@49249: blanchet@49249: signature MASH_EXPORT = blanchet@49249: sig blanchet@49266: type params = Sledgehammer_Provers.params blanchet@49250: blanchet@49545: val generate_accessibility : Proof.context -> theory -> bool -> string -> unit blanchet@49333: val generate_features : blanchet@49333: Proof.context -> string -> theory -> bool -> string -> unit blanchet@49348: val generate_isar_dependencies : blanchet@49545: Proof.context -> theory -> bool -> string -> unit blanchet@49348: val generate_atp_dependencies : blanchet@49319: Proof.context -> params -> theory -> bool -> string -> unit blanchet@49544: val generate_commands : Proof.context -> params -> theory -> string -> unit blanchet@49394: val generate_mepo_suggestions : blanchet@49266: Proof.context -> params -> theory -> int -> string -> unit blanchet@49249: end; blanchet@49249: blanchet@49249: structure MaSh_Export : MASH_EXPORT = blanchet@49249: struct blanchet@49249: blanchet@49319: open Sledgehammer_Fact blanchet@49396: open Sledgehammer_MePo blanchet@49396: open Sledgehammer_MaSh blanchet@49260: blanchet@49331: fun thy_map_from_facts ths = blanchet@49331: ths |> sort (thm_ord o swap o pairself snd) blanchet@49331: |> map (snd #> `(theory_of_thm #> Context.theory_name)) blanchet@49331: |> AList.coalesce (op =) blanchet@49393: |> map (apsnd (map nickname_of)) blanchet@49331: blanchet@49331: fun has_thy thy th = blanchet@49331: Context.theory_name thy = Context.theory_name (theory_of_thm th) blanchet@49331: blanchet@49546: fun all_non_technical_facts ctxt thy = blanchet@49546: let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in blanchet@49546: all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css blanchet@49546: |> filter_out (is_thm_technical o snd) blanchet@49546: end blanchet@49546: blanchet@49331: fun parent_facts thy thy_map = blanchet@49331: let blanchet@49331: fun add_last thy = blanchet@49331: case AList.lookup (op =) thy_map (Context.theory_name thy) of blanchet@49331: SOME (last_fact :: _) => insert (op =) last_fact blanchet@49331: | _ => add_parent thy blanchet@49331: and add_parent thy = fold add_last (Theory.parents_of thy) blanchet@49331: in add_parent thy [] end blanchet@49331: blanchet@49331: val thy_name_of_fact = hd o Long_Name.explode blanchet@49319: fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact blanchet@49319: blanchet@49453: val all_names = map (rpair () o nickname_of) #> Symtab.make blanchet@49331: blanchet@49544: fun smart_dependencies_of ctxt params prover facts all_names th = blanchet@49544: case atp_dependencies_of ctxt params prover 0 facts all_names th of blanchet@49544: SOME deps => deps blanchet@49544: | NONE => isar_dependencies_of all_names th |> these blanchet@49544: blanchet@49545: fun generate_accessibility ctxt thy include_thy file_name = blanchet@49319: let blanchet@49319: val path = file_name |> Path.explode blanchet@49319: val _ = File.write path "" blanchet@49319: fun do_fact fact prevs = blanchet@49319: let blanchet@49319: val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" blanchet@49319: val _ = File.append path s blanchet@49319: in [fact] end blanchet@49330: val thy_map = blanchet@49546: all_non_technical_facts ctxt thy blanchet@49319: |> not include_thy ? filter_out (has_thy thy o snd) blanchet@49330: |> thy_map_from_facts blanchet@49319: fun do_thy facts = blanchet@49319: let blanchet@49319: val thy = thy_of_fact thy (hd facts) blanchet@49330: val parents = parent_facts thy thy_map blanchet@49545: in fold_rev do_fact facts parents; () end blanchet@49348: in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end blanchet@49319: blanchet@49333: fun generate_features ctxt prover thy include_thy file_name = blanchet@49319: let blanchet@49319: val path = file_name |> Path.explode blanchet@49319: val _ = File.write path "" blanchet@49319: val facts = blanchet@49546: all_non_technical_facts ctxt thy blanchet@49319: |> not include_thy ? filter_out (has_thy thy o snd) blanchet@49400: fun do_fact ((_, stature), th) = blanchet@49319: let blanchet@49393: val name = nickname_of th blanchet@49333: val feats = blanchet@49400: features_of ctxt prover (theory_of_thm th) stature [prop_of th] blanchet@49319: val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" blanchet@49319: in File.append path s end blanchet@49319: in List.app do_fact facts end blanchet@49319: blanchet@49545: fun generate_isar_dependencies ctxt thy include_thy file_name = blanchet@49319: let blanchet@49319: val path = file_name |> Path.explode blanchet@49319: val _ = File.write path "" blanchet@49319: val ths = blanchet@49546: all_non_technical_facts ctxt thy blanchet@49319: |> not include_thy ? filter_out (has_thy thy o snd) blanchet@49319: |> map snd blanchet@49339: val all_names = all_names ths blanchet@49319: fun do_thm th = blanchet@49319: let blanchet@49393: val name = nickname_of th blanchet@49419: val deps = isar_dependencies_of all_names th |> these blanchet@49319: val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" blanchet@49319: in File.append path s end blanchet@49319: in List.app do_thm ths end blanchet@49319: blanchet@49407: fun generate_atp_dependencies ctxt (params as {provers, ...}) thy include_thy blanchet@49407: file_name = blanchet@49319: let blanchet@49319: val path = file_name |> Path.explode blanchet@49319: val _ = File.write path "" blanchet@49333: val prover = hd provers blanchet@49319: val facts = blanchet@49546: all_non_technical_facts ctxt thy blanchet@49319: |> not include_thy ? filter_out (has_thy thy o snd) blanchet@49319: val ths = facts |> map snd blanchet@49339: val all_names = all_names ths blanchet@49319: fun do_thm th = blanchet@49319: let blanchet@49393: val name = nickname_of th blanchet@49544: val deps = smart_dependencies_of ctxt params prover facts all_names th blanchet@49319: val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" blanchet@49319: in File.append path s end blanchet@49319: in List.app do_thm ths end blanchet@49319: blanchet@49544: fun generate_commands ctxt (params as {provers, ...}) thy file_name = blanchet@49249: let blanchet@49249: val path = file_name |> Path.explode blanchet@49249: val _ = File.write path "" blanchet@49544: val prover = hd provers blanchet@49546: val facts = all_non_technical_facts ctxt thy blanchet@49249: val (new_facts, old_facts) = blanchet@49249: facts |> List.partition (has_thy thy o snd) blanchet@49249: |>> sort (thm_ord o pairself snd) blanchet@49249: val ths = facts |> map snd blanchet@49339: val all_names = all_names ths blanchet@49400: fun do_fact ((_, stature), th) prevs = blanchet@49249: let blanchet@49393: val name = nickname_of th blanchet@49400: val feats = features_of ctxt prover thy stature [prop_of th] blanchet@49544: val deps = smart_dependencies_of ctxt params prover facts all_names th blanchet@49249: val kind = Thm.legacy_get_kind th blanchet@49544: val core = blanchet@49544: escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ blanchet@49544: escape_metas feats blanchet@49249: val query = if kind <> "" then "? " ^ core ^ "\n" else "" blanchet@49544: val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n" blanchet@49249: val _ = File.append path (query ^ update) blanchet@49249: in [name] end blanchet@49330: val thy_map = old_facts |> thy_map_from_facts blanchet@49330: val parents = parent_facts thy thy_map blanchet@49254: in fold do_fact new_facts parents; () end blanchet@49254: blanchet@49394: fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant blanchet@49307: file_name = blanchet@49254: let blanchet@49254: val path = file_name |> Path.explode blanchet@49254: val _ = File.write path "" blanchet@49333: val prover = hd provers blanchet@49546: val facts = all_non_technical_facts ctxt thy blanchet@49254: val (new_facts, old_facts) = blanchet@49254: facts |> List.partition (has_thy thy o snd) blanchet@49254: |>> sort (thm_ord o pairself snd) blanchet@49254: fun do_fact (fact as (_, th)) old_facts = blanchet@49254: let blanchet@49393: val name = nickname_of th blanchet@49265: val goal = goal_of_thm thy th blanchet@49307: val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 blanchet@49254: val kind = Thm.legacy_get_kind th blanchet@49254: val _ = blanchet@49254: if kind <> "" then blanchet@49254: let blanchet@49254: val suggs = blanchet@49307: old_facts blanchet@49421: |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover blanchet@49396: max_relevant NONE hyp_ts concl_t blanchet@49318: |> map (fn ((name, _), _) => name ()) blanchet@49318: val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" blanchet@49254: in File.append path s end blanchet@49254: else blanchet@49254: () blanchet@49254: in fact :: old_facts end blanchet@49254: in fold do_fact new_facts old_facts; () end blanchet@49249: blanchet@49249: end;