(* Title: HOL/TPTP/atp_theory_export.ML
Author: Jasmin Blanchette, TU Muenchen
Copyright 2011
Export Isabelle theories as first-order TPTP inferences.
*)
signature ATP_THEORY_EXPORT =
sig
type atp_format = ATP_Problem.atp_format
datatype inference_policy =
No_Inferences | Unchecked_Inferences | Checked_Inferences
val generate_atp_inference_file_for_theory :
Proof.context -> theory -> atp_format -> inference_policy -> string
-> string -> unit
val generate_casc_lbt_isa_files_for_theory :
Proof.context -> theory -> atp_format -> inference_policy -> string
-> string -> unit
end;
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
struct
open ATP_Problem
open ATP_Proof
open ATP_Problem_Generate
open ATP_Systems
datatype inference_policy =
No_Inferences | Unchecked_Inferences | Checked_Inferences
val fact_name_of = prefix fact_prefix o ascii_of
fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN
| atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN
| atp_for_format (DFG Polymorphic) = spass_polyN
| atp_for_format (DFG Monomorphic) = spassN
| atp_for_format (TFF (Polymorphic, _)) = alt_ergoN
| atp_for_format (TFF (Monomorphic, _)) = vampireN
| atp_for_format FOF = eN
| atp_for_format CNF_UEQ = waldmeisterN
| atp_for_format CNF = eN
val atp_timeout = seconds 0.5
fun run_atp ctxt format problem =
let
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob")
val atp = atp_for_format format
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy atp ()
val ord = effective_term_order ctxt atp
val _ = problem |> lines_for_atp_problem format ord (K [])
|> File.write_list prob_file
val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
File.shell_path (Path.explode path) ^ " " ^
arguments ctxt false "" atp_timeout (File.shell_path prob_file)
(ord, K [], K [])
val outcome =
TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command
|> fst
|> extract_tstplike_proof_and_outcome false proof_delims known_failures
|> snd
handle TimeLimit.TimeOut => SOME TimedOut
val _ =
tracing ("Ran ATP: " ^
(case outcome of
NONE => "Success"
| SOME failure => string_for_failure failure))
in outcome end
fun is_problem_line_reprovable ctxt format prelude axioms deps
(Formula (ident', _, phi, _, _)) =
is_none (run_atp ctxt format
((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
map_filter (Symtab.lookup axioms) deps) ::
prelude))
| is_problem_line_reprovable _ _ _ _ _ _ = false
fun inference_term _ [] = NONE
| inference_term check_infs ss =
ATerm (("inference", []),
[ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []),
ATerm ((tptp_empty_list, []), []),
ATerm ((tptp_empty_list, []),
map (fn s => ATerm ((s, []), [])) ss)])
|> SOME
fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
(line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
let
val deps =
case these (AList.lookup (op =) infers ident) of
[] => []
| deps =>
if check_infs andalso
not (is_problem_line_reprovable ctxt format prelude axioms deps
line) then
[]
else
deps
in
Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
end
| add_inferences_to_problem_line _ _ _ _ _ _ line = line
fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
let
fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) =
Symtab.default (ident, axiom)
| add_if_axiom _ = I
val add_axioms_of_problem = fold (fold add_if_axiom o snd)
val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem
in
map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs
prelude axioms infers))) problem
end
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
| ident_of_problem_line (Type_Decl (ident, _, _)) = ident
| ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
| ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
| ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
fun order_facts ord = sort (ord o pairself ident_of_problem_line)
fun order_problem_facts _ [] = []
| order_problem_facts ord ((heading, lines) :: problem) =
if heading = factsN then (heading, order_facts ord lines) :: problem
else (heading, lines) :: order_problem_facts ord problem
(* A fairly random selection of types used for monomorphizing. *)
val ground_types =
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
@{typ unit}]
fun ground_type_for_tvar _ [] tvar =
raise TYPE ("ground_type_for_sorts", [TVar tvar], [])
| ground_type_for_tvar thy (T :: Ts) tvar =
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
else ground_type_for_tvar thy Ts tvar
fun monomorphize_term ctxt t =
let val thy = Proof_Context.theory_of ctxt in
t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types))
handle TYPE _ => @{prop True}
end
fun heading_sort_key heading =
if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
fun problem_for_theory ctxt thy format infer_policy type_enc =
let
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val type_enc =
type_enc |> type_enc_from_string Non_Strict
|> adjust_type_enc format
val mono = not (is_type_enc_polymorphic type_enc)
val facts =
Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
Symtab.empty [] [] css_table
|> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
val problem =
facts
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
th |> prop_of |> mono ? monomorphize_term ctxt))
|> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
false true [] @{prop False}
|> #1 |> sort_wrt (heading_sort_key o fst)
val prelude = fst (split_last problem)
val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
val infers =
if infer_policy = No_Inferences then
[]
else
facts
|> map (fn (_, th) =>
(fact_name_of (Thm.get_name_hint th),
th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
|> map fact_name_of))
val all_problem_names =
problem |> maps (map ident_of_problem_line o snd)
|> distinct (op =)
val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
val infers =
infers |> filter (Symtab.defined all_problem_name_set o fst)
|> map (apsnd (filter (Symtab.defined all_problem_name_set)))
val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic
val ordered_names =
String_Graph.empty
|> fold (String_Graph.new_node o rpair ()) all_problem_names
|> fold (fn (to, froms) =>
fold (fn from => maybe_add_edge (from, to)) froms)
infers
|> fold (fn (to, from) => maybe_add_edge (from, to))
(tl all_problem_names ~~ fst (split_last all_problem_names))
|> String_Graph.topological_order
val order_tab =
Symtab.empty
|> fold (Symtab.insert (op =))
(ordered_names ~~ (1 upto length ordered_names))
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
in
problem
|> (case format of
DFG _ => I
| _ => add_inferences_to_problem ctxt format
(infer_policy = Checked_Inferences) prelude infers)
|> order_problem_facts name_ord
end
fun lines_for_problem ctxt format =
lines_for_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
fun write_lines path ss =
let
val _ = File.write path ""
val _ = app (File.append path) ss
in () end
fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
file_name =
let
val problem = problem_for_theory ctxt thy format infer_policy type_enc
val ss = lines_for_problem ctxt format problem
in write_lines (Path.explode file_name) ss end
fun ap dir = Path.append dir o Path.explode
fun chop_maximal_groups eq xs =
let
val rev_xs = rev xs
fun chop_group _ [] = []
| chop_group n (xs as x :: _) =
let
val n' = find_index (curry eq x) rev_xs
val (ws', xs') = chop (n - n') xs
in ws' :: chop_group n' xs' end
in chop_group (length xs) xs end
fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) =
(case first_field Long_Name.separator alt of
NONE => alt
| SOME (thy, _) => thy)
| theory_name_of_fact _ = ""
val problem_suffix = ".p"
val include_suffix = ".ax"
val file_order_name = "FilesInProcessingOrder"
val problem_order_name = "ProblemsInProcessingOrder"
val problem_name = "problems"
val include_name = "incl"
val prelude_base_name = "prelude"
val prelude_name = prelude_base_name ^ include_suffix
val include_base_name_of_fact = Name.desymbolize false o theory_name_of_fact
fun include_line base_name =
"include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
(* crude hack to detect theorems stated and proved by the user (as opposed to
those derived by various packages) *)
fun should_generate_problem thy (Formula ((_, alt), _, _, _, _)) =
case try (Global_Theory.get_thm thy) alt of
SOME th => Thm.legacy_get_kind th <> ""
| NONE => false
(* Convention: theoryname__goalname *)
fun problem_name_of base_name alt =
base_name ^ "__" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^
problem_suffix
fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc
dir_name =
let
val dir = Path.explode dir_name
val _ = Isabelle_System.mkdir dir
val file_order_path = ap dir file_order_name
val _ = File.write file_order_path ""
val problem_order_path = ap dir problem_order_name
val _ = File.write problem_order_path ""
val problem_dir = ap dir problem_name
val _ = Isabelle_System.mkdir problem_dir
val include_dir = ap problem_dir include_name
val _ = Isabelle_System.mkdir include_dir
val (prelude, groups) =
problem_for_theory ctxt thy format infer_policy type_enc
|> split_last
||> (snd
#> chop_maximal_groups (op = o pairself theory_name_of_fact)
#> map (`(include_base_name_of_fact o hd)))
fun write_prelude () =
let val ss = lines_for_problem ctxt format prelude in
File.append file_order_path (prelude_base_name ^ "\n");
write_lines (ap include_dir prelude_name) ss
end
fun write_include_file (base_name, facts) =
let
val name = base_name ^ include_suffix
val ss = lines_for_problem ctxt format [(factsN, facts)]
in
File.append file_order_path (base_name ^ "\n");
write_lines (ap include_dir name) ss
end
fun write_problem_files _ _ [] = ()
| write_problem_files includes [] groups =
write_problem_files includes includes groups
| write_problem_files includes _ ((base_name, []) :: groups) =
write_problem_files (includes @ [include_line base_name]) [] groups
| write_problem_files includes seen
((base_name, fact :: facts) :: groups) =
let val fact_s = tptp_string_for_line format fact in
(if should_generate_problem thy fact then
let
val (name, conj) =
(case fact of
Formula ((ident, alt), _, phi, _, _) =>
(problem_name_of base_name (Name.desymbolize false alt),
Formula ((ident, alt), Conjecture, phi, NONE, [])))
val conj_s = tptp_string_for_line format conj
in
File.append problem_order_path (name ^ "\n");
write_lines (ap problem_dir name) (seen @ [conj_s])
end
else
();
write_problem_files includes (seen @ [fact_s])
((base_name, facts) :: groups))
end
val _ = write_prelude ()
val _ = app write_include_file groups
val _ = write_problem_files [include_line prelude_base_name] [] groups
in () end
end;