don't use readable names if proof reconstruction is needed, because it uses the structure of names
authorblanchet
Mon Apr 19 11:54:07 2010 +0200 (2010-04-19 ago)
changeset 362220e3e49bd658d
parent 36221 3abbae8a10cd
child 36223 217ca1273786
don't use readable names if proof reconstruction is needed, because it uses the structure of names
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 11:02:00 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 11:54:07 2010 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4        if Config.get ctxt measure_runtime then split_time s else (s, 0)
     1.5      fun run_on probfile =
     1.6        if File.exists cmd then
     1.7 -        write_file debug full_types probfile clauses
     1.8 +        write_file full_types probfile clauses
     1.9          |> pair (apfst split_time' (bash_output (cmd_line probfile)))
    1.10        else error ("Bad executable: " ^ Path.implode cmd ^ ".");
    1.11  
    1.12 @@ -176,7 +176,8 @@
    1.13        (get_relevant_facts respect_no_atp relevance_threshold convergence
    1.14                            higher_order follow_defs max_new_clauses
    1.15                            (the_default prefers_theory_relevant theory_relevant))
    1.16 -      (prepare_clauses higher_order false) write_tptp_file command
    1.17 +      (prepare_clauses higher_order false)
    1.18 +      (write_tptp_file (overlord andalso not isar_proof)) command
    1.19        (arguments timeout) failure_strs
    1.20        (if supports_isar_proofs andalso isar_proof then
    1.21           structured_isar_proof modulus sorts
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:54:07 2010 +0200
     2.3 @@ -220,7 +220,8 @@
     2.4  type name = string * string
     2.5  type name_pool = string Symtab.table * string Symtab.table
     2.6  
     2.7 -fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
     2.8 +fun empty_name_pool readable_names =
     2.9 +  if readable_names then SOME (`I Symtab.empty) else NONE
    2.10  
    2.11  fun pool_map f xs =
    2.12    fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
    2.13 @@ -242,7 +243,7 @@
    2.14  fun translate_first_char f s =
    2.15    String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
    2.16  
    2.17 -fun clean_short_name full_name s =
    2.18 +fun readable_name full_name s =
    2.19    let
    2.20      val s = s |> Long_Name.base_name
    2.21                |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
    2.22 @@ -270,8 +271,8 @@
    2.23    | nice_name (full_name, desired_name) (SOME the_pool) =
    2.24      case Symtab.lookup (fst the_pool) full_name of
    2.25        SOME nice_name => (nice_name, SOME the_pool)
    2.26 -    | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
    2.27 -                            0 the_pool
    2.28 +    | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
    2.29 +                            the_pool
    2.30                |> apsnd SOME
    2.31  
    2.32  (**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 11:54:07 2010 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     3.5      classrel_clause list * arity_clause list ->
     3.6      int * int
     3.7 -  val write_dfg_file : bool -> bool -> Path.T ->
     3.8 +  val write_dfg_file : bool -> Path.T ->
     3.9      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    3.10      classrel_clause list * arity_clause list -> int * int
    3.11  end
    3.12 @@ -479,11 +479,11 @@
    3.13  
    3.14  (* TPTP format *)
    3.15  
    3.16 -fun write_tptp_file debug full_types file clauses =
    3.17 +fun write_tptp_file readable_names full_types file clauses =
    3.18    let
    3.19      fun section _ [] = []
    3.20        | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    3.21 -    val pool = empty_name_pool debug
    3.22 +    val pool = empty_name_pool readable_names
    3.23      val (conjectures, axclauses, _, helper_clauses,
    3.24        classrel_clauses, arity_clauses) = clauses
    3.25      val (cma, cnh) = count_constants clauses
    3.26 @@ -512,7 +512,7 @@
    3.27  
    3.28  (* DFG format *)
    3.29  
    3.30 -fun write_dfg_file debug full_types file clauses =
    3.31 +fun write_dfg_file full_types file clauses =
    3.32    let
    3.33      (* Some of the helper functions below are not name-pool-aware. However,
    3.34         there's no point in adding name pool support if the DFG format is on its