# HG changeset patch
# User blanchet
# Date 1280245391 -7200
# Node ID e207a64e1e0bb96f31e279508444330c874e635f
# Parent  ee6c11ae807759f45dbc4c3e7d5690c10968e18e
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"

diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 27 17:43:11 2010 +0200
@@ -270,6 +270,7 @@
   $(SRC)/Tools/Metis/metis.ML \
   Tools/ATP_Manager/async_manager.ML \
   Tools/ATP_Manager/atp_manager.ML \
+  Tools/ATP_Manager/atp_problem.ML \
   Tools/ATP_Manager/atp_systems.ML \
   Tools/choice_specification.ML \
   Tools/int_arith.ML \
@@ -323,7 +324,6 @@
   Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
   Tools/Sledgehammer/sledgehammer_isar.ML \
   Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
-  Tools/Sledgehammer/sledgehammer_tptp_format.ML \
   Tools/Sledgehammer/sledgehammer_util.ML \
   Tools/SMT/cvc3_solver.ML \
   Tools/SMT/smtlib_interface.ML \
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 17:43:11 2010 +0200
@@ -17,7 +17,7 @@
   ("Tools/Sledgehammer/metis_tactics.ML")
   ("Tools/Sledgehammer/sledgehammer_util.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
-  ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
+  ("Tools/ATP_Manager/atp_problem.ML")
   ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/ATP_Manager/async_manager.ML")
   ("Tools/ATP_Manager/atp_manager.ML")
@@ -94,7 +94,7 @@
 
 use "Tools/Sledgehammer/sledgehammer_util.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
+use "Tools/ATP_Manager/atp_problem.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/ATP_Manager/async_manager.ML"
 use "Tools/ATP_Manager/atp_manager.ML"
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Tools/ATP_Manager/atp_problem.ML
--- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:43:11 2010 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
+(*  Title:      HOL/Tools/ATP_Manager/atp_problem.ML
     Author:     Jia Meng, NICTA
     Author:     Jasmin Blanchette, TU Muenchen
 
 TPTP syntax.
 *)
 
-signature SLEDGEHAMMER_TPTP_FORMAT =
+signature ATP_PROBLEM =
 sig
   type kind = Metis_Clauses.kind
 
@@ -20,6 +20,7 @@
   datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
   type 'a problem = (string * 'a problem_line list) list
 
+  val timestamp : unit -> string
   val is_tptp_variable : string -> bool
   val strings_for_tptp_problem :
     (string * string problem_line list) list -> string list
@@ -29,7 +30,7 @@
        * (string Symtab.table * string Symtab.table) option
 end;
 
-structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
+structure ATP_Problem : ATP_PROBLEM =
 struct
 
 open Sledgehammer_Util
@@ -49,6 +50,8 @@
 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
 type 'a problem = (string * 'a problem_line list) list
 
+val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+
 fun string_for_term (ATerm (s, [])) = s
   | string_for_term (ATerm (s, ts)) =
     if s = "equal" then space_implode " = " (map string_for_term ts)
@@ -63,7 +66,7 @@
   | string_for_connective AIff = "<=>"
   | string_for_connective ANotIff = "<~>"
 fun string_for_formula (AQuant (q, xs, phi)) =
-    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
+    string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
     string_for_formula phi
   | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
     space_implode " != " (map string_for_term ts)
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:43:11 2010 +0200
@@ -22,7 +22,7 @@
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
+open ATP_Problem
 open Sledgehammer_Proof_Reconstruct
 open ATP_Manager
 
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Jul 27 17:43:11 2010 +0200
@@ -847,7 +847,7 @@
          out "solve "; out_outmost_f formula; out ";\n")
   in
     out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
-         "// " ^ Sledgehammer_Util.timestamp () ^ "\n");
+         "// " ^ ATP_Problem.timestamp () ^ "\n");
     map out_problem problems
   end
 
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 17:43:11 2010 +0200
@@ -29,7 +29,7 @@
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
-open Sledgehammer_TPTP_Format
+open ATP_Problem
 
 type minimize_command = string list -> string
 
diff -r ee6c11ae8077 -r e207a64e1e0b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 17:32:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 17:43:11 2010 +0200
@@ -8,7 +8,6 @@
 sig
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
-  val timestamp : unit -> string
   val strip_spaces : string -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
@@ -32,8 +31,6 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
-val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
-
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 
 fun strip_spaces_in_list [] = ""