blanchet@44064: (*  Title:      HOL/ex/atp_export.ML
blanchet@43473:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@43473:     Copyright   2011
blanchet@43473: 
blanchet@43473: Export Isabelle theories as first-order TPTP inferences, exploiting
blanchet@43473: Sledgehammer's translation.
blanchet@43473: *)
blanchet@43473: 
blanchet@44064: signature ATP_EXPORT =
blanchet@43473: sig
blanchet@44365:   val theorems_mentioned_in_proof_term :
blanchet@44365:     string list option -> thm -> string list
blanchet@43473:   val generate_tptp_graph_file_for_theory :
blanchet@43473:     Proof.context -> theory -> string -> unit
blanchet@43473:   val generate_tptp_inference_file_for_theory :
blanchet@44263:     Proof.context -> theory -> string -> string -> unit
blanchet@43473: end;
blanchet@43473: 
blanchet@44064: structure ATP_Export : ATP_EXPORT =
blanchet@43473: struct
blanchet@43473: 
blanchet@44350: open ATP_Problem
blanchet@44350: open ATP_Translate
blanchet@44428: open ATP_Proof
blanchet@44428: open ATP_Systems
blanchet@43473: 
blanchet@44350: val fact_name_of = prefix fact_prefix o ascii_of
blanchet@43473: 
blanchet@43473: fun facts_of thy =
wenzelm@44156:   Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
blanchet@44217:                                 true [] []
blanchet@44438:   |> filter (curry (op =) @{typ bool} o fastype_of
blanchet@44438:              o Object_Logic.atomize_term thy o prop_of o snd)
blanchet@43473: 
blanchet@44329: (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
blanchet@44329:    fixes that seem to be missing over there; or maybe the two code portions are
blanchet@44329:    not doing the same? *)
blanchet@44369: fun fold_body_thms thm_name all_names f =
blanchet@43473:   let
blanchet@44329:     fun app n (PBody {thms, ...}) =
blanchet@44350:       thms |> fold (fn (_, (name, prop, body)) => fn x =>
blanchet@44350:         let
blanchet@44350:           val body' = Future.join body
blanchet@44350:           val n' =
blanchet@44350:             n + (if name = "" orelse
blanchet@44350:                     (is_some all_names andalso
blanchet@44369:                      not (member (op =) (the all_names) name)) orelse
blanchet@44369:                     (* uncommon case where the proved theorem occurs twice
blanchet@44369:                        (e.g., "Transitive_Closure.trancl_into_trancl") *)
blanchet@44369:                     n = 1 andalso name = thm_name then
blanchet@44350:                    0
blanchet@44350:                  else
blanchet@44350:                    1)
blanchet@44350:           val x' = x |> n' <= 1 ? app n' body'
blanchet@44350:         in (x' |> n = 1 ? f (name, prop, body')) end)
blanchet@44350:   in fold (app 0) end
blanchet@43473: 
blanchet@44350: fun theorems_mentioned_in_proof_term all_names thm =
blanchet@43473:   let
blanchet@43473:     fun collect (s, _, _) = if s <> "" then insert (op =) s else I
blanchet@43473:     val names =
blanchet@44369:       [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect
blanchet@44369:                            [Thm.proof_body_of thm]
blanchet@44350:          |> map fact_name_of
blanchet@43473:   in names end
blanchet@43473: 
blanchet@43473: fun interesting_const_names ctxt =
wenzelm@44156:   let val thy = Proof_Context.theory_of ctxt in
blanchet@43473:     Sledgehammer_Filter.const_names_in_fact thy
blanchet@44428:         (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
blanchet@43473:   end
blanchet@43473: 
blanchet@43473: fun generate_tptp_graph_file_for_theory ctxt thy file_name =
blanchet@43473:   let
blanchet@43473:     val path = file_name |> Path.explode
blanchet@43473:     val _ = File.write path ""
blanchet@43473:     val axioms = Theory.all_axioms_of thy |> map fst
blanchet@43473:     fun do_thm thm =
blanchet@43473:       let
blanchet@43473:         val name = Thm.get_name_hint thm
blanchet@43473:         val s =
blanchet@43473:           "[" ^ Thm.legacy_get_kind thm ^ "] " ^
blanchet@43473:           (if member (op =) axioms name then "A" else "T") ^ " " ^
blanchet@44350:           prefix fact_prefix (ascii_of name) ^ ": " ^
blanchet@44350:           commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^
blanchet@44350:           commas (map (prefix const_prefix o ascii_of)
blanchet@43473:                       (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
blanchet@43473:       in File.append path s end
blanchet@44086:     val thms = facts_of thy |> map snd
blanchet@43473:     val _ = map do_thm thms
blanchet@43473:   in () end
blanchet@43473: 
blanchet@43473: fun inference_term [] = NONE
blanchet@43473:   | inference_term ss =
blanchet@44350:     ATerm ("inference",
blanchet@44350:            [ATerm ("isabelle", []),
blanchet@44350:             ATerm (tptp_empty_list, []),
blanchet@44350:             ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)])
blanchet@43473:     |> SOME
blanchet@43473: fun inference infers ident =
blanchet@43473:   these (AList.lookup (op =) infers ident) |> inference_term
blanchet@43473: fun add_inferences_to_problem_line infers
blanchet@44350:                                    (Formula (ident, Axiom, phi, NONE, NONE)) =
blanchet@44350:     Formula (ident, Lemma, phi, inference infers ident, NONE)
blanchet@43473:   | add_inferences_to_problem_line _ line = line
blanchet@43473: val add_inferences_to_problem =
blanchet@43473:   map o apsnd o map o add_inferences_to_problem_line
blanchet@43473: 
blanchet@44350: fun ident_of_problem_line (Decl (ident, _, _)) = ident
blanchet@44350:   | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
blanchet@44350: 
blanchet@44428: fun run_some_atp ctxt problem =
blanchet@44428:   let
blanchet@44428:     val thy = Proof_Context.theory_of ctxt
wenzelm@44475:     val prob_file = Path.explode "/tmp/prob.tptp"  (* FIXME File.tmp_path (?) *)
blanchet@44428:     val {exec, arguments, proof_delims, known_failures, ...} =
blanchet@44428:       get_atp thy spassN
blanchet@44428:     val _ = problem |> tptp_lines_for_atp_problem FOF
blanchet@44428:                     |> File.write_list prob_file
blanchet@44428:     val command =
blanchet@44428:       File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
blanchet@44428:       " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
blanchet@44428:       File.shell_path prob_file
blanchet@44428:   in
wenzelm@44721:     TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
blanchet@44428:     |> fst
blanchet@44428:     |> extract_tstplike_proof_and_outcome false true proof_delims
blanchet@44428:                                           known_failures
blanchet@44428:     |> snd
blanchet@44428:   end
blanchet@44428:   handle TimeLimit.TimeOut => SOME TimedOut
blanchet@44428: 
blanchet@44428: val likely_tautology_prefixes =
blanchet@44431:   [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}]
blanchet@44428:   |> map (fact_name_of o Context.theory_name)
blanchet@44428: 
blanchet@44428: fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) =
blanchet@44428:     exists (fn prefix => String.isPrefix prefix ident)
blanchet@44428:            likely_tautology_prefixes andalso
blanchet@44428:     is_none (run_some_atp ctxt
blanchet@44428:                  [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])])
blanchet@44428:   | is_problem_line_tautology _ _ = false
blanchet@44428: 
blanchet@44370: structure String_Graph = Graph(type key = string val ord = string_ord);
blanchet@44370: 
blanchet@44370: fun order_facts ord = sort (ord o pairself ident_of_problem_line)
blanchet@44370: fun order_problem_facts _ [] = []
blanchet@44370:   | order_problem_facts ord ((heading, lines) :: problem) =
blanchet@44370:     if heading = factsN then (heading, order_facts ord lines) :: problem
blanchet@44370:     else (heading, lines) :: order_problem_facts ord problem
blanchet@44370: 
blanchet@44493: fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name =
blanchet@43473:   let
blanchet@44350:     val format = FOF
blanchet@44493:     val type_enc = type_enc |> type_enc_from_string
blanchet@43473:     val path = file_name |> Path.explode
blanchet@43473:     val _ = File.write path ""
blanchet@44438:     val facts = facts_of thy
blanchet@43750:     val (atp_problem, _, _, _, _, _, _) =
blanchet@44438:       facts
blanchet@44438:       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
blanchet@44692:       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
blanchet@44733:                              (map (introduce_combinators ctxt o snd)) false true
blanchet@44733:                              [] @{prop False}
blanchet@44428:     val atp_problem =
blanchet@44428:       atp_problem
blanchet@44428:       |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
blanchet@44438:     val all_names = facts |> map (Thm.get_name_hint o snd)
blanchet@43473:     val infers =
blanchet@44438:       facts |> map (fn (_, th) =>
blanchet@44438:                        (fact_name_of (Thm.get_name_hint th),
blanchet@44438:                         theorems_mentioned_in_proof_term (SOME all_names) th))
blanchet@44350:     val all_atp_problem_names =
blanchet@44350:       atp_problem |> maps (map ident_of_problem_line o snd)
blanchet@43473:     val infers =
blanchet@44370:       infers |> filter (member (op =) all_atp_problem_names o fst)
blanchet@44370:              |> map (apsnd (filter (member (op =) all_atp_problem_names)))
blanchet@44370:     val ordered_names =
blanchet@44370:       String_Graph.empty
blanchet@44370:       |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names
blanchet@44370:       |> fold (fn (to, froms) =>
blanchet@44428:                   fold (fn from => String_Graph.add_edge (from, to)) froms)
blanchet@44428:               infers
blanchet@44370:       |> String_Graph.topological_order
blanchet@44370:     val order_tab =
blanchet@44370:       Symtab.empty
blanchet@44370:       |> fold (Symtab.insert (op =))
blanchet@44370:               (ordered_names ~~ (1 upto length ordered_names))
blanchet@44370:     val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
blanchet@44370:     val atp_problem =
blanchet@44370:       atp_problem |> add_inferences_to_problem infers
blanchet@44370:                   |> order_problem_facts name_ord
blanchet@44350:     val ss = tptp_lines_for_atp_problem FOF atp_problem
blanchet@43473:     val _ = app (File.append path) ss
blanchet@43473:   in () end
blanchet@43473: 
blanchet@43473: end;