tuned names
authorblanchet
Wed May 23 21:19:48 2012 +0200 (2012-05-23)
changeset 479766b13451135a9
parent 47975 adc977fec17e
child 47977 455a9f89c47d
tuned names
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed May 23 21:19:48 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed May 23 21:19:48 2012 +0200
     1.3 @@ -41,10 +41,10 @@
     1.4      THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
     1.5      DFG of dfg_flavor
     1.6  
     1.7 -  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
     1.8 +  datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
     1.9    datatype 'a problem_line =
    1.10      Decl of string * 'a * 'a ho_type |
    1.11 -    Formula of string * formula_kind
    1.12 +    Formula of string * formula_role
    1.13                 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    1.14                 * (string, string ho_type) ho_term option
    1.15                 * (string, string ho_type) ho_term list
    1.16 @@ -173,10 +173,10 @@
    1.17    THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
    1.18    DFG of dfg_flavor
    1.19  
    1.20 -datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.21 +datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.22  datatype 'a problem_line =
    1.23    Decl of string * 'a * 'a ho_type |
    1.24 -  Formula of string * formula_kind
    1.25 +  Formula of string * formula_role
    1.26               * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    1.27               * (string, string ho_type) ho_term option
    1.28               * (string, string ho_type) ho_term list
    1.29 @@ -310,11 +310,11 @@
    1.30    | is_format_typed (DFG DFG_Sorted) = true
    1.31    | is_format_typed _ = false
    1.32  
    1.33 -fun tptp_string_for_kind Axiom = "axiom"
    1.34 -  | tptp_string_for_kind Definition = "definition"
    1.35 -  | tptp_string_for_kind Lemma = "lemma"
    1.36 -  | tptp_string_for_kind Hypothesis = "hypothesis"
    1.37 -  | tptp_string_for_kind Conjecture = "conjecture"
    1.38 +fun tptp_string_for_role Axiom = "axiom"
    1.39 +  | tptp_string_for_role Definition = "definition"
    1.40 +  | tptp_string_for_role Lemma = "lemma"
    1.41 +  | tptp_string_for_role Hypothesis = "hypothesis"
    1.42 +  | tptp_string_for_role Conjecture = "conjecture"
    1.43  
    1.44  fun tptp_string_for_app format func args =
    1.45    if is_format_higher_order format then
    1.46 @@ -450,7 +450,7 @@
    1.47    | tptp_string_for_problem_line format
    1.48                                   (Formula (ident, kind, phi, source, _)) =
    1.49      tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
    1.50 -    tptp_string_for_kind kind ^ ",\n    (" ^
    1.51 +    tptp_string_for_role kind ^ ",\n    (" ^
    1.52      tptp_string_for_formula format phi ^ ")" ^
    1.53      (case source of
    1.54         SOME tm => ", " ^ tptp_string_for_term format tm
     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 23 21:19:48 2012 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  sig
     2.5    type term_order = ATP_Problem.term_order
     2.6    type atp_format = ATP_Problem.atp_format
     2.7 -  type formula_kind = ATP_Problem.formula_kind
     2.8 +  type formula_role = ATP_Problem.formula_role
     2.9    type failure = ATP_Proof.failure
    2.10  
    2.11    type slice_spec = int * atp_format * string * string * bool
    2.12 @@ -22,7 +22,7 @@
    2.13            * (unit -> (string * real) list) -> string,
    2.14       proof_delims : (string * string) list,
    2.15       known_failures : (failure * string) list,
    2.16 -     prem_kind : formula_kind,
    2.17 +     prem_role : formula_role,
    2.18       best_slices :
    2.19         Proof.context -> (real * (bool * (slice_spec * string))) list,
    2.20       best_max_mono_iters : int,
    2.21 @@ -60,7 +60,7 @@
    2.22    val remote_prefix : string
    2.23    val remote_atp :
    2.24      string -> string -> string list -> (string * string) list
    2.25 -    -> (failure * string) list -> formula_kind
    2.26 +    -> (failure * string) list -> formula_role
    2.27      -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
    2.28    val add_atp : string * (unit -> atp_config) -> theory -> theory
    2.29    val get_atp : theory -> string -> (unit -> atp_config)
    2.30 @@ -94,7 +94,7 @@
    2.31          * (unit -> (string * real) list) -> string,
    2.32     proof_delims : (string * string) list,
    2.33     known_failures : (failure * string) list,
    2.34 -   prem_kind : formula_kind,
    2.35 +   prem_role : formula_role,
    2.36     best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list,
    2.37     best_max_mono_iters : int,
    2.38     best_max_new_mono_instances : int}
    2.39 @@ -199,7 +199,7 @@
    2.40       [(ProofMissing, ": Valid"),
    2.41        (TimedOut, ": Timeout"),
    2.42        (GaveUp, ": Unknown")],
    2.43 -   prem_kind = Hypothesis,
    2.44 +   prem_role = Hypothesis,
    2.45     best_slices = fn _ =>
    2.46       (* FUDGE *)
    2.47       [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))],
    2.48 @@ -308,7 +308,7 @@
    2.49       [(TimedOut, "Failure: Resource limit exceeded (time)"),
    2.50        (TimedOut, "time limit exceeded")] @
    2.51       known_szs_status_failures,
    2.52 -   prem_kind = Conjecture,
    2.53 +   prem_role = Conjecture,
    2.54     best_slices = fn ctxt =>
    2.55       let val heuristic = effective_e_selection_heuristic ctxt in
    2.56         (* FUDGE *)
    2.57 @@ -340,7 +340,7 @@
    2.58       [(TimedOut, "CPU time limit exceeded, terminating"),
    2.59        (GaveUp, "No.of.Axioms")] @
    2.60       known_szs_status_failures,
    2.61 -   prem_kind = Hypothesis,
    2.62 +   prem_role = Hypothesis,
    2.63     best_slices =
    2.64       (* FUDGE *)
    2.65       K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
    2.66 @@ -363,7 +363,7 @@
    2.67     proof_delims =
    2.68       [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    2.69     known_failures = known_szs_status_failures,
    2.70 -   prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    2.71 +   prem_role = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    2.72     best_slices =
    2.73       (* FUDGE *)
    2.74       K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
    2.75 @@ -400,7 +400,7 @@
    2.76        (Unprovable, "No formulae and clauses found in input file"),
    2.77        (InternalError, "Please report this error")] @
    2.78        known_perl_failures,
    2.79 -   prem_kind = Conjecture,
    2.80 +   prem_role = Conjecture,
    2.81     best_slices = fn ctxt =>
    2.82       (* FUDGE *)
    2.83       [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))),
    2.84 @@ -425,7 +425,7 @@
    2.85       |> extra_options <> "" ? prefix (extra_options ^ " "),
    2.86     proof_delims = #proof_delims spass_old_config,
    2.87     known_failures = #known_failures spass_old_config,
    2.88 -   prem_kind = #prem_kind spass_old_config,
    2.89 +   prem_role = #prem_role spass_old_config,
    2.90     best_slices = fn _ =>
    2.91       (* FUDGE *)
    2.92       [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
    2.93 @@ -473,7 +473,7 @@
    2.94        (Unprovable, "Termination reason: Satisfiable"),
    2.95        (Interrupted, "Aborted by signal SIGINT")] @
    2.96       known_szs_status_failures,
    2.97 -   prem_kind = Conjecture,
    2.98 +   prem_role = Conjecture,
    2.99     best_slices = fn ctxt =>
   2.100       (* FUDGE *)
   2.101       (if is_new_vampire_version () then
   2.102 @@ -503,7 +503,7 @@
   2.103       "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
   2.104     proof_delims = [],
   2.105     known_failures = known_szs_status_failures,
   2.106 -   prem_kind = Hypothesis,
   2.107 +   prem_role = Hypothesis,
   2.108     best_slices =
   2.109       (* FUDGE *)
   2.110       K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
   2.111 @@ -524,7 +524,7 @@
   2.112     arguments = K (K (K (K (K "")))),
   2.113     proof_delims = [],
   2.114     known_failures = known_szs_status_failures,
   2.115 -   prem_kind = Hypothesis,
   2.116 +   prem_role = Hypothesis,
   2.117     best_slices =
   2.118       K [(1.0, (false, ((200, format, type_enc,
   2.119                          if is_format_higher_order format then keep_lamsN
   2.120 @@ -578,7 +578,7 @@
   2.121  val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   2.122  
   2.123  fun remote_config system_name system_versions proof_delims known_failures
   2.124 -                  prem_kind best_slice : atp_config =
   2.125 +                  prem_role best_slice : atp_config =
   2.126    {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
   2.127     required_vars = [],
   2.128     arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
   2.129 @@ -587,22 +587,22 @@
   2.130       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
   2.131     proof_delims = union (op =) tstp_proof_delims proof_delims,
   2.132     known_failures = known_failures @ known_perl_failures @ known_says_failures,
   2.133 -   prem_kind = prem_kind,
   2.134 +   prem_role = prem_role,
   2.135     best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))],
   2.136     best_max_mono_iters = default_max_mono_iters,
   2.137     best_max_new_mono_instances = default_max_new_mono_instances}
   2.138  
   2.139  fun remotify_config system_name system_versions best_slice
   2.140 -        ({proof_delims, known_failures, prem_kind, ...} : atp_config)
   2.141 +        ({proof_delims, known_failures, prem_role, ...} : atp_config)
   2.142          : atp_config =
   2.143    remote_config system_name system_versions proof_delims known_failures
   2.144 -                prem_kind best_slice
   2.145 +                prem_role best_slice
   2.146  
   2.147  fun remote_atp name system_name system_versions proof_delims known_failures
   2.148 -               prem_kind best_slice =
   2.149 +               prem_role best_slice =
   2.150    (remote_prefix ^ name,
   2.151     fn () => remote_config system_name system_versions proof_delims
   2.152 -                          known_failures prem_kind best_slice)
   2.153 +                          known_failures prem_role best_slice)
   2.154  fun remotify_atp (name, config) system_name system_versions best_slice =
   2.155    (remote_prefix ^ name,
   2.156     remotify_config system_name system_versions best_slice o config)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 23 21:19:48 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 23 21:19:48 2012 +0200
     3.3 @@ -855,6 +855,7 @@
     3.4  (* FIXME: make more reliable *)
     3.5  val exists_low_level_class_const =
     3.6    exists_Const (fn (s, _) =>
     3.7 +     s = @{const_name equal_class.equal} orelse
     3.8       String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
     3.9  
    3.10  fun is_metastrange_theorem th =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 23 21:19:48 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 23 21:19:48 2012 +0200
     4.3 @@ -584,7 +584,7 @@
     4.4  
     4.5  fun run_atp mode name
     4.6          ({exec, required_vars, arguments, proof_delims, known_failures,
     4.7 -          prem_kind, best_slices, best_max_mono_iters,
     4.8 +          prem_role, best_slices, best_max_mono_iters,
     4.9            best_max_new_mono_instances, ...} : atp_config)
    4.10          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    4.11                      uncurried_aliases, max_relevant, max_mono_iters,
    4.12 @@ -720,7 +720,7 @@
    4.13                      |> polymorphism_of_type_enc type_enc <> Polymorphic
    4.14                         ? monomorphize_facts
    4.15                      |> map (apsnd prop_of)
    4.16 -                    |> prepare_atp_problem ctxt format prem_kind type_enc
    4.17 +                    |> prepare_atp_problem ctxt format prem_role type_enc
    4.18                                             atp_mode lam_trans uncurried_aliases
    4.19                                             readable_names true hyp_ts concl_t
    4.20                  fun sel_weights () = atp_problem_selection_weights atp_problem