# 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 =