complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
authorblanchet
Tue Jul 27 17:43:11 2010 +0200 (2010-07-27)
changeset 38019e207a64e1e0b
parent 38018 ee6c11ae8077
child 38020 badd89633f4c
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_problem.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 27 17:32:55 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 27 17:43:11 2010 +0200
     1.3 @@ -270,6 +270,7 @@
     1.4    $(SRC)/Tools/Metis/metis.ML \
     1.5    Tools/ATP_Manager/async_manager.ML \
     1.6    Tools/ATP_Manager/atp_manager.ML \
     1.7 +  Tools/ATP_Manager/atp_problem.ML \
     1.8    Tools/ATP_Manager/atp_systems.ML \
     1.9    Tools/choice_specification.ML \
    1.10    Tools/int_arith.ML \
    1.11 @@ -323,7 +324,6 @@
    1.12    Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
    1.13    Tools/Sledgehammer/sledgehammer_isar.ML \
    1.14    Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
    1.15 -  Tools/Sledgehammer/sledgehammer_tptp_format.ML \
    1.16    Tools/Sledgehammer/sledgehammer_util.ML \
    1.17    Tools/SMT/cvc3_solver.ML \
    1.18    Tools/SMT/smtlib_interface.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:32:55 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 17:43:11 2010 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4    ("Tools/Sledgehammer/metis_tactics.ML")
     2.5    ("Tools/Sledgehammer/sledgehammer_util.ML")
     2.6    ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
     2.7 -  ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
     2.8 +  ("Tools/ATP_Manager/atp_problem.ML")
     2.9    ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
    2.10    ("Tools/ATP_Manager/async_manager.ML")
    2.11    ("Tools/ATP_Manager/atp_manager.ML")
    2.12 @@ -94,7 +94,7 @@
    2.13  
    2.14  use "Tools/Sledgehammer/sledgehammer_util.ML"
    2.15  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    2.16 -use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
    2.17 +use "Tools/ATP_Manager/atp_problem.ML"
    2.18  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    2.19  use "Tools/ATP_Manager/async_manager.ML"
    2.20  use "Tools/ATP_Manager/atp_manager.ML"
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:32:55 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 17:43:11 2010 +0200
     3.3 @@ -1,11 +1,11 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
     3.5 +(*  Title:      HOL/Tools/ATP_Manager/atp_problem.ML
     3.6      Author:     Jia Meng, NICTA
     3.7      Author:     Jasmin Blanchette, TU Muenchen
     3.8  
     3.9  TPTP syntax.
    3.10  *)
    3.11  
    3.12 -signature SLEDGEHAMMER_TPTP_FORMAT =
    3.13 +signature ATP_PROBLEM =
    3.14  sig
    3.15    type kind = Metis_Clauses.kind
    3.16  
    3.17 @@ -20,6 +20,7 @@
    3.18    datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
    3.19    type 'a problem = (string * 'a problem_line list) list
    3.20  
    3.21 +  val timestamp : unit -> string
    3.22    val is_tptp_variable : string -> bool
    3.23    val strings_for_tptp_problem :
    3.24      (string * string problem_line list) list -> string list
    3.25 @@ -29,7 +30,7 @@
    3.26         * (string Symtab.table * string Symtab.table) option
    3.27  end;
    3.28  
    3.29 -structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
    3.30 +structure ATP_Problem : ATP_PROBLEM =
    3.31  struct
    3.32  
    3.33  open Sledgehammer_Util
    3.34 @@ -49,6 +50,8 @@
    3.35  datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
    3.36  type 'a problem = (string * 'a problem_line list) list
    3.37  
    3.38 +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    3.39 +
    3.40  fun string_for_term (ATerm (s, [])) = s
    3.41    | string_for_term (ATerm (s, ts)) =
    3.42      if s = "equal" then space_implode " = " (map string_for_term ts)
    3.43 @@ -63,7 +66,7 @@
    3.44    | string_for_connective AIff = "<=>"
    3.45    | string_for_connective ANotIff = "<~>"
    3.46  fun string_for_formula (AQuant (q, xs, phi)) =
    3.47 -    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
    3.48 +    string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
    3.49      string_for_formula phi
    3.50    | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
    3.51      space_implode " != " (map string_for_term ts)
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:32:55 2010 +0200
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:43:11 2010 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  open Metis_Clauses
     4.5  open Sledgehammer_Util
     4.6  open Sledgehammer_Fact_Filter
     4.7 -open Sledgehammer_TPTP_Format
     4.8 +open ATP_Problem
     4.9  open Sledgehammer_Proof_Reconstruct
    4.10  open ATP_Manager
    4.11  
     5.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Jul 27 17:32:55 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Jul 27 17:43:11 2010 +0200
     5.3 @@ -847,7 +847,7 @@
     5.4           out "solve "; out_outmost_f formula; out ";\n")
     5.5    in
     5.6      out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
     5.7 -         "// " ^ Sledgehammer_Util.timestamp () ^ "\n");
     5.8 +         "// " ^ ATP_Problem.timestamp () ^ "\n");
     5.9      map out_problem problems
    5.10    end
    5.11  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 17:32:55 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 17:43:11 2010 +0200
     6.3 @@ -29,7 +29,7 @@
     6.4  open Metis_Clauses
     6.5  open Sledgehammer_Util
     6.6  open Sledgehammer_Fact_Filter
     6.7 -open Sledgehammer_TPTP_Format
     6.8 +open ATP_Problem
     6.9  
    6.10  type minimize_command = string list -> string
    6.11  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 17:32:55 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jul 27 17:43:11 2010 +0200
     7.3 @@ -8,7 +8,6 @@
     7.4  sig
     7.5    val plural_s : int -> string
     7.6    val serial_commas : string -> string list -> string list
     7.7 -  val timestamp : unit -> string
     7.8    val strip_spaces : string -> string
     7.9    val parse_bool_option : bool -> string -> string -> bool option
    7.10    val parse_time_option : string -> string -> Time.time option
    7.11 @@ -32,8 +31,6 @@
    7.12    | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    7.13    | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    7.14  
    7.15 -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    7.16 -
    7.17  fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    7.18  
    7.19  fun strip_spaces_in_list [] = ""