--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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 =
--- 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 =