# HG changeset patch # User blanchet # Date 1384455250 -3600 # Node ID e275d520f49d634c8692b8a41f830320280a54b0 # Parent b1721e5b87173d2186fed6b73a9a3b85da8b467f implemented 'tptp_translate' diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Thu Nov 14 19:54:10 2013 +0100 @@ -7,23 +7,20 @@ signature ATP_PROBLEM_IMPORT = sig - val read_tptp_file : - theory -> (term -> term) -> string - -> term list * (term list * term list) * Proof.context + val read_tptp_file : theory -> (string * term -> 'a) -> string -> + 'a list * ('a list * 'a list) * Proof.context val nitpick_tptp_file : theory -> int -> string -> unit val refute_tptp_file : theory -> int -> string -> unit val can_tac : Proof.context -> tactic -> term -> bool val SOLVE_TIMEOUT : int -> string -> tactic -> tactic - val atp_tac : - Proof.context -> int -> (string * string) list -> int -> string -> int - -> tactic + val atp_tac : Proof.context -> int -> (string * string) list -> int -> string -> int -> tactic val smt_solver_tac : string -> Proof.context -> int -> tactic val freeze_problem_consts : theory -> term -> term val make_conj : term list * term list -> term list -> term val sledgehammer_tptp_file : theory -> int -> string -> unit val isabelle_tptp_file : theory -> int -> string -> unit val isabelle_hot_tptp_file : theory -> int -> string -> unit - val translate_tptp_file : string -> string -> string -> unit + val translate_tptp_file : theory -> string -> string -> string -> unit end; structure ATP_Problem_Import : ATP_PROBLEM_IMPORT = @@ -32,6 +29,8 @@ open ATP_Util open ATP_Problem open ATP_Proof +open ATP_Problem_Generate +open ATP_Systems val debug = false val overlord = false @@ -39,16 +38,18 @@ (** TPTP parsing **) +fun exploded_absolute_path file_name = + Path.explode file_name + |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD")) + fun read_tptp_file thy postproc file_name = let fun has_role role (_, role', _, _) = (role' = role) - fun get_prop (_, _, P, _) = - P |> Logic.varify_global |> close_form |> postproc - val path = - Path.explode file_name - |> (fn path => - path |> not (Path.is_absolute path) - ? Path.append (Path.explode "$PWD")) + fun get_prop (name, role, P, info) = + let val P' = P |> Logic.varify_global |> close_form in + (name, P') |> postproc + end + val path = exploded_absolute_path file_name val ((_, _, problem), thy) = TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy @@ -68,7 +69,7 @@ fun nitpick_tptp_file thy timeout file_name = let - val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name + val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name val thy = Proof_Context.theory_of ctxt val (defs, pseudo_defs) = defs |> map (ATP_Util.abs_extensionalize_term ctxt @@ -115,7 +116,7 @@ else "Unknown") |> Output.urgent_message - val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name + val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] @@ -272,7 +273,7 @@ fun sledgehammer_tptp_file thy timeout file_name = let val (conjs, assms, ctxt) = - read_tptp_file thy (freeze_problem_consts thy) file_name + read_tptp_file thy (freeze_problem_consts thy o snd) file_name val conj = make_conj assms conjs in can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj @@ -282,7 +283,7 @@ fun generic_isabelle_tptp_file demo thy timeout file_name = let val (conjs, assms, ctxt) = - read_tptp_file thy (freeze_problem_consts thy) file_name + read_tptp_file thy (freeze_problem_consts thy o snd) file_name val conj = make_conj assms conjs val (last_hope_atp, last_hope_completeness) = if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2) @@ -300,6 +301,33 @@ (** Translator between TPTP(-like) file formats **) -fun translate_tptp_file format in_file_name out_file_name = () +fun translate_tptp_file thy format_str in_file_name out_file_name = + let + val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I in_file_name + val conj = make_conj ([], []) (map snd conjs) + + val (format, type_enc, lam_trans) = + (case format_str of + "FOF" => (FOF, "mono_guards??", liftingN) + | "TFF0" => (TFF Monomorphic, "mono_native", liftingN) + | "THF0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN) + | "DFG" => (DFG Monomorphic, "mono_native", liftingN) + | _ => error ("Unknown format " ^ quote format_str ^ + " (expected \"FOF\", \"TFF0\", \"THF0\", or \"DFG\")")) + val uncurried_aliases = false + val readable_names = true + val presimp = true + val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @ + map (apfst (rpair (Global, General))) nondefs + val (atp_problem, _, _, _, _) = + prepare_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator + lam_trans uncurried_aliases readable_names presimp [] conj facts + + val ord = effective_term_order ctxt spassN + val ord_info = K [] + val lines = lines_of_atp_problem format ord ord_info atp_problem + in + File.write_list (exploded_absolute_path out_file_name) lines + end end; diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_isabelle --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Thu Nov 14 19:54:10 2013 +0100 @@ -29,5 +29,5 @@ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy - "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Thu Nov 14 19:54:10 2013 +0100 @@ -29,5 +29,5 @@ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy - "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_nitpick --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Thu Nov 14 19:54:10 2013 +0100 @@ -29,5 +29,5 @@ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy - "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_refute --- a/src/HOL/TPTP/lib/Tools/tptp_refute Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute Thu Nov 14 19:54:10 2013 +0100 @@ -28,5 +28,5 @@ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy - "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Thu Nov 14 19:54:10 2013 +0100 @@ -29,5 +29,5 @@ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ > /tmp/$SCRATCH.thy - "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" + "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r b1721e5b8717 -r e275d520f49d src/HOL/TPTP/lib/Tools/tptp_translate --- a/src/HOL/TPTP/lib/Tools/tptp_translate Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate Thu Nov 14 19:54:10 2013 +0100 @@ -11,7 +11,7 @@ echo echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE" echo - echo " Translates TPTP input file to specified TPTP format (\"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")." + echo " Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")." echo exit 1 } @@ -23,6 +23,6 @@ args=("$@") echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.translate_tptp_file \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ +ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ > /tmp/$SCRATCH.thy -"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" +"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" diff -r b1721e5b8717 -r e275d520f49d src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 14 19:54:10 2013 +0100 @@ -15,7 +15,7 @@ type atp_formula_role = ATP_Problem.atp_formula_role type 'a atp_problem = 'a ATP_Problem.atp_problem - datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter + datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = @@ -127,7 +127,7 @@ open ATP_Util open ATP_Problem -datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter +datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = @@ -2756,12 +2756,11 @@ val app_op_and_predicator_threshold = 45 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans - uncurried_aliases readable_names preproc hyp_ts concl_t + uncurried_aliases readable_names presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format - val exporter = (mode = Exporter) val completish = (mode = Sledgehammer_Completish) (* Forcing explicit applications is expensive for polymorphic encodings, because it takes only one existential variable ranging over "'a => 'b" to @@ -2778,7 +2777,7 @@ if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN else lam_trans val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = - translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts concl_t facts + translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish val ctrss = all_ctrss_of_datatypes thy @@ -2811,10 +2810,12 @@ val datatype_decl_lines = map decl_line_of_datatype datatypes val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines val num_facts = length facts + val freshen = mode <> Exporter andalso mode <> Translator + val pos = mode <> Exporter + val rank_of = rank_of_fact_num num_facts val fact_lines = - map (line_of_fact ctxt fact_prefix ascii_of I (not exporter) - (not exporter) mono type_enc (rank_of_fact_num num_facts)) - (0 upto num_facts - 1 ~~ facts) + map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of) + (0 upto num_facts - 1 ~~ facts) val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses val helper_lines = diff -r b1721e5b8717 -r e275d520f49d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Nov 14 16:10:31 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Nov 14 19:54:10 2013 +0100 @@ -505,9 +505,9 @@ them each time. *) val atp_important_message_keep_quotient = 25 -fun choose_type_enc soundness best_type_enc format = +fun choose_type_enc strictness best_type_enc format = the_default best_type_enc - #> type_enc_of_string soundness + #> type_enc_of_string strictness #> adjust_type_enc format fun isar_proof_reconstructor ctxt name = @@ -663,9 +663,9 @@ Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge |> Integer.min (length facts) - val soundness = if strict then Strict else Non_Strict + val strictness = if strict then Strict else Non_Strict val type_enc = - type_enc |> choose_type_enc soundness best_type_enc format + type_enc |> choose_type_enc strictness best_type_enc format val sound = is_type_enc_sound type_enc val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout =