--- 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 \
--- 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"
--- 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)
--- 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
--- 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
--- 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
--- 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 [] = ""