added options to Sledgehammer;
syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Mar 23 11:39:21 2010 +0100
@@ -12,9 +12,11 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
- (thm * (string * int)) list
- val prepare_clauses : bool -> thm list -> thm list ->
+ val get_relevant_facts :
+ real -> bool option -> bool -> int -> bool
+ -> Proof.context * (thm list * 'a) -> thm list
+ -> (thm * (string * int)) list
+ val prepare_clauses : bool option -> bool -> thm list -> thm list ->
(thm * (axiom_name * hol_clause_id)) list ->
(thm * (axiom_name * hol_clause_id)) list -> theory ->
axiom_name vector *
@@ -38,20 +40,11 @@
(* and also explicit ATP invocation methods *)
(********************************************************************)
-(* Translation mode can be auto-detected, or forced to be first-order or
- higher-order *)
-datatype mode = Auto | Fol | Hol;
-
-val translation_mode = Auto;
-
(*** background linkup ***)
val run_blacklist_filter = true;
(*** relevance filter parameters ***)
-val run_relevance_filter = true;
-val pass_mark = 0.5;
val convergence = 3.2; (*Higher numbers allow longer inference chains*)
-val follow_defs = false; (*Follow definitions. Makes problems bigger.*)
(***************************************************************)
(* Relevance Filtering *)
@@ -139,8 +132,8 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun const_prop_of theory_const th =
- if theory_const then
+fun const_prop_of add_theory_const th =
+ if add_theory_const then
let val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ ". 1", HOLogic.boolT)
in t $ prop_of th end
@@ -169,7 +162,7 @@
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
-fun count_axiom_consts theory_const thy ((thm,_), tab) =
+fun count_axiom_consts add_theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
let val (c, cts) = const_with_typ thy (a,T)
in (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -182,7 +175,7 @@
count_term_consts (t, count_term_consts (u, tab))
| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
| count_term_consts (_, tab) = tab
- in count_term_consts (const_prop_of theory_const thm, tab) end;
+ in count_term_consts (const_prop_of add_theory_const thm, tab) end;
(**** Actual Filtering Code ****)
@@ -214,8 +207,8 @@
let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
in Symtab.fold add_expand_pairs tab [] end;
-fun pair_consts_typs_axiom theory_const thy (thm,name) =
- ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) =
+ (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm)));
exception ConstFree;
fun dest_ConstFree (Const aT) = aT
@@ -234,9 +227,10 @@
end
handle ConstFree => false
in
- case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
+ case tm of
+ @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
+ defs lhs rhs
+ | _ => false
end;
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
@@ -263,7 +257,7 @@
end
end;
-fun relevant_clauses max_new thy ctab p rel_consts =
+fun relevant_clauses follow_defs max_new thy ctab p rel_consts =
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
| relevant (newpairs,rejects) [] =
let val (newrels,more_rejects) = take_best max_new newpairs
@@ -273,7 +267,8 @@
in
trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
(map #1 newrels) @
- (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
+ (relevant_clauses follow_defs max_new thy ctab newp rel_consts'
+ (more_rejects @ rejects))
end
| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
let val weight = clause_weight ctab rel_consts consts_typs
@@ -288,20 +283,27 @@
relevant ([],[])
end;
-fun relevance_filter max_new theory_const thy axioms goals =
- if run_relevance_filter andalso pass_mark >= 0.1
- then
- let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+fun relevance_filter relevance_threshold follow_defs max_new add_theory_const
+ thy axioms goals =
+ if relevance_threshold >= 0.1 then
+ let
+ val const_tab = List.foldl (count_axiom_consts add_theory_const thy)
+ Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = trace_msg (fn () => ("Initial constants: " ^
- space_implode ", " (Symtab.keys goal_const_tab)));
- val rels = relevant_clauses max_new thy const_tab (pass_mark)
- goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
- in
- trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
- rels
- end
- else axioms;
+ val _ =
+ trace_msg (fn () => "Initial constants: " ^
+ commas (Symtab.keys goal_const_tab))
+ val relevant =
+ relevant_clauses follow_defs max_new thy const_tab
+ relevance_threshold goal_const_tab
+ (map (pair_consts_typs_axiom add_theory_const thy)
+ axioms)
+ in
+ trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
+ relevant
+ end
+ else
+ axioms;
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -526,34 +528,35 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-fun is_first_order thy goal_cls =
- case translation_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
- | Fol => true
- | Hol => false
+fun is_first_order thy higher_order goal_cls =
+ case higher_order of
+ NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | SOME b => not b
-fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
+ add_theory_const (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val included_cls = get_all_lemmas ctxt
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
in
- relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ relevance_filter relevance_threshold follow_defs max_new add_theory_const
+ thy included_cls (map prop_of goal_cls)
end;
(* prepare for passing to writer,
create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
let
(* add chain thms *)
val chain_cls =
cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_first_order thy higher_order goal_cls
val ccls = subtract_cls goal_cls extra_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Mar 23 11:39:21 2010 +0100
@@ -51,9 +51,9 @@
conclusion variable to False.*)
fun transform_elim th =
case concl_of th of (*conclusion variable*)
- Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, Type("prop",[])) =>
+ | v as Var(_, @{typ prop}) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
| _ => th;
@@ -76,7 +76,7 @@
fun declare_skofuns s th =
let
val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
@@ -95,20 +95,20 @@
Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
- | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
+ | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
in dec_sko (subst_bound (Free (fname, T), p)) thx end
- | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
- | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
| dec_sko t thx = thx (*Do nothing otherwise*)
in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns s th =
let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
+ fun dec_sko (Const (@{const_name "Ex"}, _) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
@@ -123,13 +123,13 @@
in dec_sko (subst_bound (list_comb(c,args), p))
(def :: defs)
end
- | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
| dec_sko t defs = defs (*Do nothing otherwise*)
in dec_sko (prop_of th) [] end;
@@ -156,7 +156,7 @@
fun strip_lambdas 0 th = th
| strip_lambdas n th =
case prop_of th of
- _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+ _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;
@@ -171,7 +171,7 @@
let
val thy = theory_of_cterm ct
val Abs(x,_,body) = term_of ct
- val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
in
@@ -262,8 +262,9 @@
val (chilbert,cabs) = Thm.dest_comb ch
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
- val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
- | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+ val T = case t of
+ Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
+ | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
@@ -289,7 +290,7 @@
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
+(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
val max_lambda_nesting = 3;
@@ -320,7 +321,8 @@
fun is_strange_thm th =
case head_of (concl_of th) of
- Const (a, _) => (a <> "Trueprop" andalso a <> "==")
+ Const (a, _) => (a <> @{const_name Trueprop} andalso
+ a <> @{const_name "=="})
| _ => false;
fun bad_for_atp th =
@@ -328,9 +330,10 @@
orelse exists_type type_has_topsort (prop_of th)
orelse is_strange_thm th;
+(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
- ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *)
+ ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+ "split_asm", "cases", "ext_cases"];
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Mar 23 11:39:21 2010 +0100
@@ -48,7 +48,7 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-(* Parameter t_full below indicates that full type information is to be
+(* Parameter "full_types" below indicates that full type information is to be
exported *)
(* If true, each function will be directly applied to as many arguments as
@@ -210,10 +210,8 @@
fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
| head_needs_hBOOL _ _ = true;
-fun wrap_type t_full (s, tp) =
- if t_full then
- type_wrapper ^ paren_pack [s, string_of_fol_type tp]
- else s;
+fun wrap_type full_types (s, tp) =
+ if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
fun apply ss = "hAPP" ^ paren_pack ss;
@@ -224,7 +222,7 @@
(*Apply an operator to the argument strings, using either the "apply" operator or
direct function application.*)
-fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
+fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
let val c = if c = "equal" then "c_fequal" else c
val nargs = min_arity_of cma c
val args1 = List.take(args, nargs)
@@ -232,21 +230,22 @@
Int.toString nargs ^ " but is applied to " ^
space_implode ", " args)
val args2 = List.drop(args, nargs)
- val targs = if not t_full then map string_of_fol_type tvars else []
+ val targs = if full_types then [] else map string_of_fol_type tvars
in
string_apply (c ^ paren_pack (args1@targs), args2)
end
| string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
| string_of_applic _ _ _ = error "string_of_applic";
-fun wrap_type_if t_full cnh (head, s, tp) =
- if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
+fun wrap_type_if full_types cnh (head, s, tp) =
+ if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
-fun string_of_combterm (params as (t_full, cma, cnh)) t =
+fun string_of_combterm (params as (full_types, cma, cnh)) t =
let val (head, args) = strip_combterm_comb t
- in wrap_type_if t_full cnh (head,
- string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
- type_of_combterm t)
+ in wrap_type_if full_types cnh (head,
+ string_of_applic full_types cma
+ (head, map (string_of_combterm (params)) args),
+ type_of_combterm t)
end;
(*Boolean-valued terms are here converted to literals.*)
@@ -318,11 +317,11 @@
fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
-fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
+fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
- val ntys = if not t_full then length tvars else 0
+ 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 (addtypes tvars (addit funcs), preds)
@@ -452,12 +451,12 @@
(* TPTP format *)
-fun write_tptp_file t_full file clauses =
+fun write_tptp_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
val _ =
@@ -474,12 +473,12 @@
(* DFG format *)
-fun write_dfg_file t_full file clauses =
+fun write_dfg_file full_types file clauses =
let
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
- val params = (t_full, cma, cnh)
+ val params = (full_types, cma, cnh)
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
and probname = Path.implode (Path.base file)
val axstrs = map (#1 o (clause2dfg params)) axclauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 23 11:39:21 2010 +0100
@@ -4,43 +4,125 @@
Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
*)
+signature SLEDGEHAMMER_ISAR =
+sig
+ type params = ATP_Manager.params
+
+ val default_params : theory -> (string * string) list -> params
+end;
+
structure Sledgehammer_Isar : sig end =
struct
open ATP_Manager
open ATP_Minimal
+open Sledgehammer_Util
structure K = OuterKeyword and P = OuterParse
-val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+type raw_param = string * string list
+
+val default_default_params =
+ [("debug", "false"),
+ ("verbose", "false"),
+ ("relevance_threshold", "0.5"),
+ ("higher_order", "smart"),
+ ("respect_no_atp", "true"),
+ ("follow_defs", "false"),
+ ("isar_proof", "false"),
+ ("minimize_timeout", "5 s")]
+
+val negated_params =
+ [("no_debug", "debug"),
+ ("quiet", "verbose"),
+ ("partial_types", "full_types"),
+ ("first_order", "higher_order"),
+ ("ignore_no_atp", "respect_no_atp"),
+ ("dont_follow_defs", "follow_defs"),
+ ("metis_proof", "isar_proof")]
+
+val property_affected_params = ["atps", "full_types", "timeout"]
-val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+fun is_known_raw_param s =
+ AList.defined (op =) default_default_params s orelse
+ AList.defined (op =) negated_params s orelse
+ member (op =) property_affected_params s
+
+fun check_raw_param (s, _) =
+ if is_known_raw_param s then ()
+ else error ("Unknown parameter: " ^ quote s ^ ".")
-val _ =
- OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
- (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
- (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+fun unnegate_raw_param (name, value) =
+ case AList.lookup (op =) negated_params name of
+ SOME name' => (name', case value of
+ ["false"] => ["true"]
+ | ["true"] => ["false"]
+ | [] => ["false"]
+ | _ => value)
+ | NONE => (name, value)
+
+structure Data = Theory_Data(
+ type T = raw_param list
+ val empty = default_default_params |> map (apsnd single)
+ val extend = I
+ fun merge p : T = AList.merge (op =) (K true) p)
-val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+fun default_raw_params thy =
+ [("atps", [!atps]),
+ ("full_types", [if !full_types then "true" else "false"]),
+ ("timeout", [string_of_int (!timeout) ^ " s"])] @
+ Data.get thy
+
+val infinity_time_in_secs = 60 * 60 * 24 * 365
+val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
-val _ =
- OuterSyntax.improper_command "sledgehammer"
- "search for first-order proof using automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+fun extract_params thy default_params override_params =
+ let
+ val override_params = map unnegate_raw_param override_params
+ val raw_params = rev override_params @ rev default_params
+ val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+ val lookup_string = the_default "" o lookup
+ fun general_lookup_bool option default_value name =
+ case lookup name of
+ SOME s => s |> parse_bool_option option name
+ | NONE => default_value
+ val lookup_bool = the o general_lookup_bool false (SOME false)
+ val lookup_bool_option = general_lookup_bool true NONE
+ fun lookup_time name =
+ the_timeout (case lookup name of
+ NONE => NONE
+ | SOME s => parse_time_option name s)
+ fun lookup_real name =
+ case lookup name of
+ NONE => 0.0
+ | SOME s => 0.0 (* FIXME ### *)
+ val debug = lookup_bool "debug"
+ val verbose = debug orelse lookup_bool "verbose"
+ val atps = lookup_string "atps" |> space_explode " "
+ val full_types = lookup_bool "full_types"
+ val relevance_threshold = lookup_real "relevance_threshold"
+ val higher_order = lookup_bool_option "higher_order"
+ val respect_no_atp = lookup_bool "respect_no_atp"
+ val follow_defs = lookup_bool "follow_defs"
+ val isar_proof = lookup_bool "isar_proof"
+ val timeout = lookup_time "timeout"
+ val minimize_timeout = lookup_time "minimize_timeout"
+ in
+ {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
+ relevance_threshold = relevance_threshold, higher_order = higher_order,
+ respect_no_atp = respect_no_atp, follow_defs = follow_defs,
+ isar_proof = isar_proof, timeout = timeout,
+ minimize_timeout = minimize_timeout}
+ end
-val default_minimize_prover = "remote_vampire"
-val default_minimize_time_limit = 5
+fun default_params thy =
+ extract_params thy (default_raw_params thy) o map (apsnd single)
fun atp_minimize_command args thm_names state =
let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
fun theorems_from_names ctxt =
map (fn (name, interval) =>
let
@@ -48,40 +130,104 @@
val ths = ProofContext.get_fact ctxt thmref
val name' = Facts.string_of_ref thmref
in (name', ths) end)
- fun get_time_limit_arg time_string =
- (case Int.fromString time_string of
- SOME t => t
- | NONE => error ("Invalid time limit: " ^ quote time_string))
+ fun get_time_limit_arg s =
+ (case Int.fromString s of
+ SOME t => Time.fromSeconds t
+ | NONE => error ("Invalid time limit: " ^ quote s))
fun get_opt (name, a) (p, t) =
(case name of
"time" => (p, get_time_limit_arg a)
| "atp" => (a, t)
| n => error ("Invalid argument: " ^ n))
- fun get_options args =
- fold get_opt args (default_minimize_prover, default_minimize_time_limit)
- val (prover_name, time_limit) = get_options args
+ val {atps, minimize_timeout, ...} = default_params thy []
+ fun get_options args = fold get_opt args (hd atps, minimize_timeout)
+ val (atp, timeout) = get_options args
+ val params =
+ default_params thy
+ [("atps", atp),
+ ("minimize_timeout", string_of_int (Time.toSeconds timeout) ^ " s")]
val prover =
- (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+ (case get_prover thy atp of
SOME prover => prover
- | NONE => error ("Unknown prover: " ^ quote prover_name))
- val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+ | NONE => error ("Unknown ATP: " ^ quote atp))
+ val name_thms_pairs = theorems_from_names ctxt thm_names
in
- writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
- state name_thms_pairs))
+ writeln (#2 (minimize_theorems params linear_minimize prover atp state
+ name_thms_pairs))
end
-local structure K = OuterKeyword and P = OuterParse in
-
val parse_args =
Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
-
val _ =
- OuterSyntax.improper_command "atp_minimize" "minimize theorem list with external prover" K.diag
+ OuterSyntax.improper_command "atp_minimize"
+ "minimize theorem list with external prover" K.diag
(parse_args -- parse_thm_names >> (fn (args, thm_names) =>
Toplevel.no_timing o Toplevel.unknown_proof o
Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
-end
+fun hammer_away override_params i state =
+ let
+ val thy = Proof.theory_of state
+ val _ = List.app check_raw_param override_params
+ val params = extract_params thy (default_raw_params thy) override_params
+ in sledgehammer params i state end
+
+fun sledgehammer_trans (opt_params, opt_i) =
+ Toplevel.keep (hammer_away (these opt_params) (the_default 1 opt_i)
+ o Toplevel.proof_of)
+
+fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+
+fun sledgehammer_params_trans opt_params =
+ Toplevel.theory
+ (fold set_default_raw_param (these opt_params)
+ #> tap (fn thy =>
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case rev (default_raw_params thy) of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))))
+
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_value =
+ Scan.repeat1 (P.minus >> single
+ || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat
+val parse_param =
+ parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)
+val parse_params =
+ Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")
+val parse_sledgehammer_command =
+ (parse_params -- Scan.option P.nat) #>> sledgehammer_trans
+val parse_sledgehammer_params_command =
+ parse_params #>> sledgehammer_params_trans
+
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill))
+val _ =
+ OuterSyntax.improper_command "atp_info"
+ "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info))
+val _ =
+ OuterSyntax.improper_command "atp_messages"
+ "print recent messages issued by managed provers" K.diag
+ (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+ (fn limit => Toplevel.no_timing
+ o Toplevel.imperative (fn () => messages limit)))
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (print_provers o Toplevel.theory_of)))
+val _ =
+ OuterSyntax.improper_command "sledgehammer"
+ "search for first-order proof using automatic theorem provers" K.diag
+ parse_sledgehammer_command
+val _ =
+ OuterSyntax.command "sledgehammer_params"
+ "set and display the default parameters for Sledgehammer" K.thy_decl
+ parse_sledgehammer_params_command
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 15:23:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Mar 23 11:39:21 2010 +0100
@@ -540,9 +540,10 @@
(* atp_minimize [atp=<prover>] <lemmas> *)
fun minimize_line _ [] = ""
- | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
- Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
- space_implode " " (kill_chained lemmas))
+ | minimize_line name lemmas =
+ "To minimize the number of lemmas, try this command:\n" ^
+ Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
+ space_implode " " (kill_chained lemmas))
fun metis_lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
@@ -570,8 +571,11 @@
if member (op =) tokens chained_hint then ""
else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
in
- (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
- lemma_names)
+ (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
+ for a strange ProofGeneral bug, whereby the first two letters of the word
+ "proof" are not highlighted. *)
+ (one_line_proof ^ "\n\nStructured proof:" ^
+ Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
end
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Mar 23 11:39:21 2010 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/Sledgehammer/sledgehammer_util.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+General-purpose functions used by the Sledgehammer modules.
+*)
+
+signature SLEDGEHAMMER_UTIL =
+sig
+ val serial_commas : string -> string list -> string list
+ val parse_bool_option : bool -> string -> string -> bool option
+ val parse_time_option : string -> string -> Time.time option
+end;
+
+structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
+struct
+
+fun serial_commas _ [] = ["??"]
+ | serial_commas _ [s] = [s]
+ | serial_commas conj [s1, s2] = [s1, conj, s2]
+ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+ | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
+fun parse_bool_option option name s =
+ (case s of
+ "smart" => if option then NONE else raise Option
+ | "false" => SOME false
+ | "true" => SOME true
+ | "" => SOME true
+ | _ => raise Option)
+ handle Option.Option =>
+ let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+ error ("Parameter " ^ quote name ^ " must be assigned " ^
+ space_implode " " (serial_commas "or" ss) ^ ".")
+ end
+
+fun parse_time_option _ "none" = NONE
+ | parse_time_option name s =
+ let
+ val msecs =
+ case space_explode " " s of
+ [s1, "min"] => 60000 * the (Int.fromString s1)
+ | [s1, "s"] => 1000 * the (Int.fromString s1)
+ | [s1, "ms"] => the (Int.fromString s1)
+ | _ => 0
+ in
+ if msecs <= 0 then
+ error ("Parameter " ^ quote name ^ " must be assigned a positive time \
+ \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
+ else
+ SOME (Time.fromMilliseconds msecs)
+ end
+
+end;