src/HOL/Tools/ATP_Manager/atp_problem.ML
 changeset 38019 e207a64e1e0b parent 38018 ee6c11ae8077 child 38024 e4a95eb5530e
1.1 --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:32:55 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:43:11 2010 +0200
1.3 @@ -1,11 +1,11 @@
1.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
1.5 +(*  Title:      HOL/Tools/ATP_Manager/atp_problem.ML
1.6      Author:     Jia Meng, NICTA
1.7      Author:     Jasmin Blanchette, TU Muenchen
1.9  TPTP syntax.
1.10  *)
1.12 -signature SLEDGEHAMMER_TPTP_FORMAT =
1.13 +signature ATP_PROBLEM =
1.14  sig
1.15    type kind = Metis_Clauses.kind
1.17 @@ -20,6 +20,7 @@
1.18    datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
1.19    type 'a problem = (string * 'a problem_line list) list
1.21 +  val timestamp : unit -> string
1.22    val is_tptp_variable : string -> bool
1.23    val strings_for_tptp_problem :
1.24      (string * string problem_line list) list -> string list
1.25 @@ -29,7 +30,7 @@
1.26         * (string Symtab.table * string Symtab.table) option
1.27  end;
1.29 -structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
1.30 +structure ATP_Problem : ATP_PROBLEM =
1.31  struct
1.33  open Sledgehammer_Util
1.34 @@ -49,6 +50,8 @@
1.35  datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
1.36  type 'a problem = (string * 'a problem_line list) list
1.38 +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
1.39 +
1.40  fun string_for_term (ATerm (s, [])) = s
1.41    | string_for_term (ATerm (s, ts)) =
1.42      if s = "equal" then space_implode " = " (map string_for_term ts)
1.43 @@ -63,7 +66,7 @@
1.44    | string_for_connective AIff = "<=>"
1.45    | string_for_connective ANotIff = "<~>"
1.46  fun string_for_formula (AQuant (q, xs, phi)) =
1.47 -    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
1.48 +    string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
1.49      string_for_formula phi
1.50    | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
1.51      space_implode " != " (map string_for_term ts)