src/HOL/TPTP/atp_theory_export.ML
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62549 9498623b27f0
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/TPTP/atp_theory_export.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2011
     4 
     5 Export Isabelle theories as first-order TPTP inferences.
     6 *)
     7 
     8 signature ATP_THEORY_EXPORT =
     9 sig
    10   type atp_format = ATP_Problem.atp_format
    11 
    12   datatype inference_policy =
    13     No_Inferences | Unchecked_Inferences | Checked_Inferences
    14 
    15   val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format ->
    16     inference_policy -> string -> string -> unit
    17   val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format ->
    18     inference_policy -> string -> string -> unit
    19 end;
    20 
    21 structure ATP_Theory_Export : ATP_THEORY_EXPORT =
    22 struct
    23 
    24 open ATP_Problem
    25 open ATP_Proof
    26 open ATP_Problem_Generate
    27 open ATP_Systems
    28 
    29 val max_dependencies = 100
    30 val max_facts = 512
    31 val atp_timeout = seconds 0.5
    32 
    33 datatype inference_policy =
    34   No_Inferences | Unchecked_Inferences | Checked_Inferences
    35 
    36 val prefix = Library.prefix
    37 val fact_name_of = prefix fact_prefix o ascii_of
    38 
    39 fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
    40   | atp_of_format (THF (Monomorphic, _)) = satallaxN
    41   | atp_of_format (DFG Polymorphic) = pirateN
    42   | atp_of_format (DFG Monomorphic) = spassN
    43   | atp_of_format (TFF Polymorphic) = alt_ergoN
    44   | atp_of_format (TFF Monomorphic) = vampireN
    45   | atp_of_format FOF = eN
    46   | atp_of_format CNF_UEQ = waldmeisterN
    47   | atp_of_format CNF = eN
    48 
    49 fun run_atp ctxt format problem =
    50   let
    51     val thy = Proof_Context.theory_of ctxt
    52     val prob_file = File.tmp_path (Path.explode "prob")
    53     val atp = atp_of_format format
    54     val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp ()
    55     val ord = effective_term_order ctxt atp
    56     val _ = problem
    57       |> lines_of_atp_problem format ord (K [])
    58       |> File.write_list prob_file
    59     val exec = exec false
    60     val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
    61     val command =
    62       File.bash_path (Path.explode path) ^ " " ^
    63       arguments ctxt false "" atp_timeout (File.bash_path prob_file)
    64                 (ord, K [], K [])
    65     val outcome =
    66       Timeout.apply atp_timeout Isabelle_System.bash_output command
    67       |> fst
    68       |> extract_tstplike_proof_and_outcome false proof_delims known_failures
    69       |> snd
    70       handle Timeout.TIMEOUT _ => SOME TimedOut
    71     val _ =
    72       tracing ("Ran ATP: " ^
    73                (case outcome of
    74                   NONE => "Success"
    75                 | SOME failure => string_of_atp_failure failure))
    76   in outcome end
    77 
    78 fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) =
    79     is_none (run_atp ctxt format
    80       ((factsN,
    81         Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) ::
    82        prelude))
    83   | is_problem_line_reprovable _ _ _ _ _ _ = false
    84 
    85 fun inference_term _ [] = NONE
    86   | inference_term check_infs ss =
    87     ATerm (("inference", []),
    88         [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []),
    89          ATerm ((tptp_empty_list, []), []),
    90          ATerm ((tptp_empty_list, []),
    91          map (fn s => ATerm ((s, []), [])) ss)])
    92     |> SOME
    93 
    94 fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
    95       (line as Formula ((ident, alt), Axiom, phi, NONE, info)) =
    96     let
    97       val deps =
    98         case these (AList.lookup (op =) infers ident) of
    99           [] => []
   100         | deps =>
   101           if check_infs andalso
   102              not (is_problem_line_reprovable ctxt format prelude axioms deps
   103                                              line) then
   104             []
   105           else
   106             deps
   107     in
   108       Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info)
   109     end
   110   | add_inferences_to_problem_line _ _ _ _ _ _ line = line
   111 
   112 fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
   113   let
   114     fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom)
   115       | add_if_axiom _ = I
   116 
   117     val add_axioms_of_problem = fold (fold add_if_axiom o snd)
   118     val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem
   119   in
   120     map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers)))
   121       problem
   122   end
   123 
   124 fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
   125   | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
   126   | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
   127   | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
   128   | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
   129 
   130 fun order_facts ord = sort (ord o apply2 ident_of_problem_line)
   131 
   132 fun order_problem_facts _ [] = []
   133   | order_problem_facts ord ((heading, lines) :: problem) =
   134     if heading = factsN then (heading, order_facts ord lines) :: problem
   135     else (heading, lines) :: order_problem_facts ord problem
   136 
   137 (* A fairly random selection of types used for monomorphizing. *)
   138 val ground_types =
   139   [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
   140    @{typ unit}]
   141 
   142 fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], [])
   143   | ground_type_of_tvar thy (T :: Ts) tvar =
   144     if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
   145     else ground_type_of_tvar thy Ts tvar
   146 
   147 fun monomorphize_term ctxt t =
   148   let val thy = Proof_Context.theory_of ctxt in
   149     t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types))
   150     handle TYPE _ => @{prop True}
   151   end
   152 
   153 fun heading_sort_key heading =
   154   if String.isPrefix factsN heading then "_" ^ heading else heading
   155 
   156 fun problem_of_theory ctxt thy format infer_policy type_enc =
   157   let
   158     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   159     val type_enc =
   160       type_enc |> type_enc_of_string Non_Strict
   161                |> adjust_type_enc format
   162     val mono = not (is_type_enc_polymorphic type_enc)
   163 
   164     val facts =
   165       Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
   166                                   Keyword.empty_keywords [] [] css_table
   167       |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
   168     val problem =
   169       facts
   170       |> map (fn ((_, loc), th) =>
   171         ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
   172       |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
   173         @{prop False}
   174       |> #1 |> sort_by (heading_sort_key o fst)
   175     val prelude = fst (split_last problem)
   176     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
   177     val infers =
   178       if infer_policy = No_Inferences then
   179         []
   180       else
   181         facts
   182         |> map (fn (_, th) =>
   183                    (fact_name_of (Thm.get_name_hint th),
   184                     th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
   185                        |> these |> map fact_name_of))
   186     val all_problem_names =
   187       problem |> maps (map ident_of_problem_line o snd) |> distinct (op =)
   188     val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
   189     val infers =
   190       infers |> filter (Symtab.defined all_problem_name_set o fst)
   191              |> map (apsnd (filter (Symtab.defined all_problem_name_set)))
   192     val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic
   193     val ordered_names =
   194       String_Graph.empty
   195       |> fold (String_Graph.new_node o rpair ()) all_problem_names
   196       |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers
   197       |> fold (fn (to, from) => maybe_add_edge (from, to))
   198         (tl all_problem_names ~~ fst (split_last all_problem_names))
   199       |> String_Graph.topological_order
   200     val order_tab =
   201       Symtab.empty
   202       |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
   203     val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab)
   204   in
   205     (facts,
   206      problem
   207      |> (case format of
   208           DFG _ => I
   209         | _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude
   210           infers)
   211      |> order_problem_facts name_ord)
   212   end
   213 
   214 fun lines_of_problem ctxt format =
   215   lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
   216 
   217 fun write_lines path ss =
   218   let
   219     val _ = File.write path ""
   220     val _ = app (File.append path) ss
   221   in () end
   222 
   223 fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
   224                                            file_name =
   225   let
   226     val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc
   227     val ss = lines_of_problem ctxt format problem
   228   in write_lines (Path.explode file_name) ss end
   229 
   230 fun ap dir = Path.append dir o Path.explode
   231 
   232 fun chop_maximal_groups eq xs =
   233   let
   234     val rev_xs = rev xs
   235     fun chop_group _ [] = []
   236       | chop_group n (xs as x :: _) =
   237         let
   238           val n' = find_index (curry eq x) rev_xs
   239           val (ws', xs') = chop (n - n') xs
   240         in ws' :: chop_group n' xs' end
   241    in chop_group (length xs) xs end
   242 
   243 fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) =
   244     (case first_field Long_Name.separator alt of
   245        NONE => alt
   246      | SOME (thy, _) => thy)
   247   | theory_name_of_fact _ = ""
   248 
   249 val problem_suffix = ".p"
   250 val suggestion_suffix = ".sugg"
   251 val include_suffix = ".ax"
   252 
   253 val file_order_name = "FilesInProcessingOrder"
   254 val problem_order_name = "ProblemsInProcessingOrder"
   255 val problem_name = "problems"
   256 val suggestion_name = "suggestions"
   257 val include_name = "incl"
   258 val prelude_base_name = "prelude"
   259 val prelude_name = prelude_base_name ^ include_suffix
   260 
   261 val encode_meta = Sledgehammer_MaSh.encode_str
   262 
   263 fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x)
   264 
   265 fun include_line base_name =
   266   "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
   267 
   268 val hol_base_name = encode_meta "HOL"
   269 
   270 fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
   271   (case try (Global_Theory.get_thm thy) alt of
   272     SOME th =>
   273     (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those
   274        derived by various packages). In addition, we leave out everything in "HOL" as too basic to
   275        be interesting. *)
   276     Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
   277   | NONE => false)
   278 
   279 (* Convention: theoryname__goalname *)
   280 fun problem_name_of base_name n alt =
   281   base_name ^ "__" ^ string_of_int n ^ "_" ^
   282   perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix
   283 
   284 fun suggestion_name_of base_name n alt =
   285   base_name ^ "__" ^ string_of_int n ^ "_" ^
   286   perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix
   287 
   288 fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name =
   289   let
   290     val dir = Path.explode dir_name
   291     val _ = Isabelle_System.mkdir dir
   292     val file_order_path = ap dir file_order_name
   293     val _ = File.write file_order_path ""
   294     val problem_order_path = ap dir problem_order_name
   295     val _ = File.write problem_order_path ""
   296     val problem_dir = ap dir problem_name
   297     val _ = Isabelle_System.mkdir problem_dir
   298     val suggestion_dir = ap dir suggestion_name
   299     val _ = Isabelle_System.mkdir suggestion_dir
   300     val include_dir = ap problem_dir include_name
   301     val _ = Isabelle_System.mkdir include_dir
   302 
   303     val (facts, (prelude, groups)) =
   304       problem_of_theory ctxt thy format infer_policy type_enc
   305       ||> split_last
   306       ||> apsnd (snd
   307            #> chop_maximal_groups (op = o apply2 theory_name_of_fact)
   308            #> map (`(include_base_name_of_fact o hd)))
   309 
   310     val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts)
   311 
   312     fun write_prelude () =
   313       let val ss = lines_of_problem ctxt format prelude in
   314         File.append file_order_path (prelude_base_name ^ "\n");
   315         write_lines (ap include_dir prelude_name) ss
   316       end
   317 
   318     fun write_include_file (base_name, fact_lines) =
   319       let
   320         val name = base_name ^ include_suffix
   321         val ss = lines_of_problem ctxt format [(factsN, fact_lines)]
   322       in
   323         File.append file_order_path (base_name ^ "\n");
   324         write_lines (ap include_dir name) ss
   325       end
   326 
   327     fun select_facts_for_fact facts fact =
   328       let
   329         val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact))
   330         val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt
   331           (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts
   332       in
   333         map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo
   334       end
   335 
   336     fun write_problem_files _ _ _ _ [] = ()
   337       | write_problem_files _ seen_facts includes [] groups =
   338         write_problem_files 1 seen_facts includes includes groups
   339       | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) =
   340         write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups
   341       | write_problem_files n seen_facts includes seen_ss
   342           ((base_name, fact_line :: fact_lines) :: groups) =
   343         let
   344           val (alt, pname, sname, conj) =
   345             (case fact_line of
   346               Formula ((ident, alt), _, phi, _, _) =>
   347               (alt, problem_name_of base_name n (encode_meta alt),
   348                suggestion_name_of base_name n (encode_meta alt),
   349                Formula ((ident, alt), Conjecture, phi, NONE, [])))
   350           val fact = the (Symtab.lookup fact_tab alt)
   351           val fact_s = tptp_string_of_line format fact_line
   352         in
   353           (if should_generate_problem thy base_name fact_line then
   354              let
   355                val conj_s = tptp_string_of_line format conj
   356              in
   357                File.append problem_order_path (pname ^ "\n");
   358                write_lines (ap problem_dir pname) (seen_ss @ [conj_s]);
   359                write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact)
   360              end
   361            else
   362              ();
   363            write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s])
   364              ((base_name, fact_lines) :: groups))
   365         end
   366 
   367     val _ = write_prelude ()
   368     val _ = app write_include_file groups
   369     val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups
   370   in () end
   371 
   372 end;