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.8  
     1.9  TPTP syntax.
    1.10  *)
    1.11  
    1.12 -signature SLEDGEHAMMER_TPTP_FORMAT =
    1.13 +signature ATP_PROBLEM =
    1.14  sig
    1.15    type kind = Metis_Clauses.kind
    1.16  
    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.20  
    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.28  
    1.29 -structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
    1.30 +structure ATP_Problem : ATP_PROBLEM =
    1.31  struct
    1.32  
    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.37  
    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)