author blanchet Wed May 23 21:19:48 2012 +0200 (2012-05-23) changeset 47976 6b13451135a9 parent 47975 adc977fec17e child 47977 455a9f89c47d
tuned names
```     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