--- a/src/HOL/TPTP/atp_problem_import.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Tue Jun 26 11:14:40 2012 +0200
@@ -183,19 +183,19 @@
in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
end
-fun atp_tac ctxt aggressivity override_params timeout prover =
+fun atp_tac ctxt completeness override_params timeout prover =
let
val ctxt =
- ctxt |> Config.put Sledgehammer_Provers.aggressive (aggressivity > 0)
+ ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0)
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
([("debug", if debug then "true" else "false"),
("overlord", if overlord then "true" else "false"),
("provers", prover),
("timeout", string_of_int timeout)] @
- (if aggressivity > 0 then
+ (if completeness > 0 then
[("type_enc",
- if aggressivity = 1 then "mono_native" else "poly_guards??"),
+ if completeness = 1 then "mono_native" else "poly_guards??"),
("slicing", "false")]
else
[]) @
@@ -207,12 +207,12 @@
fun sledgehammer_tac demo ctxt timeout i =
let
val frac = if demo then 16 else 12
- fun slice mult aggressivity prover =
+ fun slice mult completeness prover =
SOLVE_TIMEOUT (mult * timeout div frac)
(prover ^
- (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
+ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")"
else ""))
- (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
+ (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
in
slice 2 0 ATP_Systems.spassN
ORELSE slice 2 0 ATP_Systems.vampireN
@@ -290,13 +290,13 @@
val (conjs, assms, ctxt) =
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
- val (last_hope_atp, last_hope_aggressive) =
+ val (last_hope_atp, last_hope_completeness) =
if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
- (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj)
+ (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
|> print_szs_from_success conjs
end
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -492,11 +492,14 @@
fun string_of_arity (0, n) = string_of_int n
| string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n
+val dfg_class_inter = space_implode " & "
+
fun dfg_string_for_formula poly gen_simp info =
let
val str_for_typ = string_for_type (DFG poly)
fun str_for_bound_typ (ty, []) = str_for_typ ty
- | str_for_bound_typ (ty, cls) = str_for_typ ty ^ " : " ^ commas cls
+ | str_for_bound_typ (ty, cls) =
+ str_for_typ ty ^ " : " ^ dfg_class_inter cls
fun suffix_tag top_level s =
if top_level then
case extract_isabelle_status info of
@@ -554,7 +557,7 @@
|>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
fun str_for_bound_tvar (ty, []) = ty
- | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ commas cls
+ | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
fun sort_decl xs ty cl =
"sort(" ^
(if null xs then ""
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -15,7 +15,7 @@
type formula_role = ATP_Problem.formula_role
type 'a problem = 'a ATP_Problem.problem
- datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
+ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
datatype scope = Global | Local | Assum | Chained
datatype status =
@@ -116,7 +116,7 @@
open ATP_Util
open ATP_Problem
-datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
+datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
datatype scope = Global | Local | Assum | Chained
datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
@@ -1594,8 +1594,8 @@
val predicator_iconst =
IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
-fun predicatify aggressive tm =
- if aggressive then
+fun predicatify completish tm =
+ if completish then
IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm),
fTrue_iconst)
else
@@ -1615,7 +1615,7 @@
in list_app app [head, arg] end
fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases
- aggressive =
+ completish =
let
fun do_app arg head = mk_app_op type_enc head arg
fun list_app_ops head args = fold do_app args head
@@ -1637,8 +1637,8 @@
fun introduce_predicators tm =
case strip_iterm_comb tm of
(IConst ((s, _), _, _), _) =>
- if is_pred_sym sym_tab s then tm else predicatify aggressive tm
- | _ => predicatify aggressive tm
+ if is_pred_sym sym_tab s then tm else predicatify completish tm
+ | _ => predicatify completish tm
val do_iterm =
not (is_type_enc_higher_order type_enc)
? (introduce_app_ops #> introduce_predicators)
@@ -1699,7 +1699,7 @@
[(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
|> map (apsnd (map (apsnd zero_var_indexes)))
-val aggressive_helper_table =
+val completish_helper_table =
base_helper_table @
[((predicator_name, true),
@{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
@@ -1761,7 +1761,7 @@
could_specialize_helpers type_enc andalso
not (null (Term.hidden_polymorphism t))
-fun add_helper_facts_for_sym ctxt format type_enc aggressive
+fun add_helper_facts_for_sym ctxt format type_enc completish
(s, {types, ...} : sym_info) =
case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
@@ -1794,18 +1794,18 @@
fold (fn ((helper_s, needs_sound), ths) =>
if (needs_sound andalso not sound) orelse
(helper_s <> unmangled_s andalso
- (not aggressive orelse could_specialize)) then
+ (not completish orelse could_specialize)) then
I
else
ths ~~ (1 upto length ths)
|> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
|> make_facts
|> union (op = o pairself #iformula))
- (if aggressive then aggressive_helper_table else helper_table)
+ (if completish then completish_helper_table else helper_table)
end
| NONE => I
-fun helper_facts_for_sym_table ctxt format type_enc aggressive sym_tab =
- Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc aggressive)
+fun helper_facts_for_sym_table ctxt format type_enc completish sym_tab =
+ Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc completish)
sym_tab []
(***************************************************************)
@@ -2253,13 +2253,13 @@
end
(* We add "bool" in case the helper "True_or_False" is included later. *)
-fun default_mono level aggressive =
+fun default_mono level completish =
{maybe_finite_Ts = [@{typ bool}],
surely_infinite_Ts =
case level of
Nonmono_Types (Strict, _) => []
| _ => known_infinite_types,
- maybe_nonmono_Ts = [if aggressive then tvar_a else @{typ bool}]}
+ maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
out with monotonicity" paper presented at CADE 2011. *)
@@ -2291,9 +2291,9 @@
fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
formula_fold (SOME (role <> Conjecture))
(add_iterm_mononotonicity_info ctxt level) iformula
-fun mononotonicity_info_for_facts ctxt type_enc aggressive facts =
+fun mononotonicity_info_for_facts ctxt type_enc completish facts =
let val level = level_of_type_enc type_enc in
- default_mono level aggressive
+ default_mono level completish
|> is_type_level_monotonicity_based level
? fold (add_fact_mononotonicity_info ctxt level) facts
end
@@ -2655,7 +2655,7 @@
ruin everything. Hence we do it only if there are few facts (which is
normally the case for "metis" and the minimizer). *)
val app_op_level =
- if mode = Sledgehammer_Aggressive then
+ if mode = Sledgehammer_Completish then
Full_App_Op_And_Predicator
else if length facts + length hyp_ts
> app_op_and_predicator_threshold then
@@ -2664,7 +2664,7 @@
else
Sufficient_App_Op_And_Predicator
val exporter = (mode = Exporter)
- val aggressive = (mode = Sledgehammer_Aggressive)
+ val completish = (mode = Sledgehammer_Completish)
val lam_trans =
if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
@@ -2678,11 +2678,11 @@
val (_, sym_tab0) =
sym_table_for_facts ctxt type_enc app_op_level conjs facts
val mono =
- conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc aggressive
+ conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc completish
val constrs = all_constrs_of_polymorphic_datatypes thy
fun firstorderize in_helper =
firstorderize_fact thy constrs type_enc sym_tab0
- (uncurried_aliases andalso not in_helper) aggressive
+ (uncurried_aliases andalso not in_helper) completish
val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
val (ho_stuff, sym_tab) =
sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
@@ -2694,7 +2694,7 @@
|> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
uncurried_alias_eq_tms
val helpers =
- sym_tab |> helper_facts_for_sym_table ctxt format type_enc aggressive
+ sym_tab |> helper_facts_for_sym_table ctxt format type_enc completish
|> map (firstorderize true)
val mono_Ts =
helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:40 2012 +0200
@@ -65,7 +65,7 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
- val aggressive : bool Config.T
+ val completish : bool Config.T
val atp_full_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -335,8 +335,8 @@
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
val problem_prefix =
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val aggressive =
- Attrib.setup_config_bool @{binding sledgehammer_aggressive} (K false)
+val completish =
+ Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
(* In addition to being easier to read, readable names are often much shorter,
especially if types are mangled in names. This makes a difference for some
@@ -596,7 +596,7 @@
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val atp_mode =
- if Config.get ctxt aggressive then Sledgehammer_Aggressive
+ if Config.get ctxt completish then Sledgehammer_Completish
else Sledgehammer
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val (dest_dir, problem_prefix) =