added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 16:04:36 2010 +0200
@@ -15,6 +15,7 @@
overlord: bool,
atps: string list,
full_types: bool,
+ explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
convergence: real,
@@ -69,6 +70,7 @@
overlord: bool,
atps: string list,
full_types: bool,
+ explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
convergence: real,
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 16:04:36 2010 +0200
@@ -67,7 +67,7 @@
| (failure :: _) => SOME failure
fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
- proof_text name ({debug, full_types, ...} : params)
+ proof_text name ({debug, full_types, explicit_apply, ...} : params)
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -128,7 +128,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write_file full_types probfile clauses
+ write_file full_types explicit_apply probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd ^ ".");
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 16:04:36 2010 +0200
@@ -34,10 +34,10 @@
val get_helper_clauses : bool -> theory -> bool ->
hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
hol_clause list
- val write_tptp_file : bool -> bool -> Path.T ->
+ val write_tptp_file : bool -> bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list -> unit
- val write_dfg_file : bool -> Path.T ->
+ val write_dfg_file : bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list -> unit
end
@@ -50,19 +50,19 @@
open Sledgehammer_Fact_Preprocessor
(* Parameter "full_types" below indicates that full type information is to be
-exported *)
+ exported.
-(* If true, each function will be directly applied to as many arguments as
- possible, avoiding use of the "apply" operator. Use of hBOOL is also
- minimized. *)
-val minimize_applies = true;
+ If "explicit_apply" is false, each function will be directly applied to as
+ many arguments as possible, avoiding use of the "apply" operator. Use of
+ hBOOL is also minimized.
+*)
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
(*True if the constant ever appears outside of the top-level position in literals.
If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL const_needs_hBOOL c =
- not minimize_applies orelse
+fun needs_hBOOL explicit_apply const_needs_hBOOL c =
+ explicit_apply orelse
the_default false (Symtab.lookup const_needs_hBOOL c);
@@ -211,9 +211,10 @@
val type_wrapper = "ti";
-fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
- needs_hBOOL const_needs_hBOOL c
- | head_needs_hBOOL _ _ = true;
+fun head_needs_hBOOL explicit_apply const_needs_hBOOL
+ (CombConst ((c, _), _, _)) =
+ needs_hBOOL explicit_apply const_needs_hBOOL c
+ | head_needs_hBOOL _ _ _ = true
fun wrap_type full_types (s, ty) pool =
if full_types then
@@ -223,8 +224,11 @@
else
(s, pool)
-fun wrap_type_if full_types cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
+fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
+ if head_needs_hBOOL explicit_apply cnh head then
+ wrap_type full_types (s, tp)
+ else
+ pair s
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -252,18 +256,22 @@
| string_of_application _ _ (CombVar (name, _), args) pool =
nice_name name pool |>> (fn s => string_apply (s, args))
-fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
+fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
+ pool =
let
val (head, args) = strip_combterm_comb t
val (ss, pool) = pool_map (string_of_combterm params) args pool
val (s, pool) = string_of_application full_types cma (head, ss) pool
- in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
+ in
+ wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
+ pool
+ end
(*Boolean-valued terms are here converted to literals.*)
fun boolify params c =
string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
-fun string_of_predicate (params as (_, _, cnh)) t =
+fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
case t of
(CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
(* DFG only: new TPTP prefers infix equality *)
@@ -272,7 +280,8 @@
| _ =>
case #1 (strip_combterm_comb t) of
CombConst ((s, _), _, _) =>
- (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
+ (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
+ params t
| _ => boolify params t
@@ -342,8 +351,8 @@
fun add_types tvars = fold add_fol_type_funcs tvars
-fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars))
- (funcs, preds) =
+fun add_decls (full_types, explicit_apply, cma, cnh)
+ (CombConst ((c, _), _, tvars)) (funcs, preds) =
if c = "equal" then
(add_types tvars funcs, preds)
else
@@ -351,8 +360,10 @@
val ntys = if not full_types then length tvars else 0
val addit = Symtab.update(c, arity+ntys)
in
- if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds)
- else (add_types tvars funcs, addit preds)
+ if needs_hBOOL explicit_apply cnh c then
+ (add_types tvars (addit funcs), preds)
+ else
+ (add_types tvars funcs, addit preds)
end
| add_decls _ (CombVar (_, ctp)) (funcs, preds) =
(add_fol_type_funcs ctp funcs, preds)
@@ -458,18 +469,23 @@
(const_min_arity, const_needs_hBOOL) =
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
-fun display_arity const_needs_hBOOL (c,n) =
+fun display_arity explicit_apply const_needs_hBOOL (c,n) =
trace_msg (fn () => "Constant: " ^ c ^
" arity:\t" ^ Int.toString n ^
- (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
+ (if needs_hBOOL explicit_apply const_needs_hBOOL c then
+ " needs hBOOL"
+ else
+ ""))
-fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
- if minimize_applies then
+fun count_constants explicit_apply
+ (conjectures, _, extra_clauses, helper_clauses, _, _) =
+ if not explicit_apply then
let val (const_min_arity, const_needs_hBOOL) =
fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
|> fold count_constants_clause extra_clauses
|> fold count_constants_clause helper_clauses
- val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
+ val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
+ (Symtab.dest (const_min_arity))
in (const_min_arity, const_needs_hBOOL) end
else (Symtab.empty, Symtab.empty);
@@ -479,15 +495,15 @@
(* TPTP format *)
-fun write_tptp_file readable_names full_types file clauses =
+fun write_tptp_file readable_names full_types explicit_apply file clauses =
let
fun section _ [] = []
| section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
val pool = empty_name_pool readable_names
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants clauses
- val params = (full_types, cma, cnh)
+ val (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
@@ -511,7 +527,7 @@
(* DFG format *)
-fun write_dfg_file full_types file clauses =
+fun write_dfg_file full_types explicit_apply file clauses =
let
(* Some of the helper functions below are not name-pool-aware. However,
there's no point in adding name pool support if the DFG format is on its
@@ -519,8 +535,8 @@
val pool = NONE
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
- val (cma, cnh) = count_constants clauses
- val params = (full_types, cma, cnh)
+ val (cma, cnh) = count_constants explicit_apply clauses
+ val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
and probname = Path.implode (Path.base file)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 16:04:36 2010 +0200
@@ -41,6 +41,7 @@
[("debug", "false"),
("verbose", "false"),
("overlord", "false"),
+ ("explicit_apply", "false"),
("respect_no_atp", "true"),
("relevance_threshold", "50"),
("convergence", "320"),
@@ -58,6 +59,7 @@
[("no_debug", "debug"),
("quiet", "verbose"),
("no_overlord", "overlord"),
+ ("implicit_apply", "explicit_apply"),
("ignore_no_atp", "respect_no_atp"),
("partial_types", "full_types"),
("theory_irrelevant", "theory_relevant"),
@@ -146,6 +148,7 @@
val overlord = lookup_bool "overlord"
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
+ val explicit_apply = lookup_bool "explicit_apply"
val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
@@ -160,11 +163,12 @@
val minimize_timeout = lookup_time "minimize_timeout"
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
- full_types = full_types, respect_no_atp = respect_no_atp,
- relevance_threshold = relevance_threshold, convergence = convergence,
- theory_relevant = theory_relevant, higher_order = higher_order,
- follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
- sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
+ full_types = full_types, explicit_apply = explicit_apply,
+ respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ convergence = convergence, theory_relevant = theory_relevant,
+ higher_order = higher_order, follow_defs = follow_defs,
+ isar_proof = isar_proof, modulus = modulus, sorts = sorts,
+ timeout = timeout, minimize_timeout = minimize_timeout}
end
fun get_params thy = extract_params thy (default_raw_params thy)