# HG changeset patch # User blanchet # Date 1269340761 -3600 # Node ID 943e2582dc87312eefc24b332cde6487af362299 # Parent 0e2d57686b3ce9bc7a7346570190f6e4d8946797 added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- 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); diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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 diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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; diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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=] *) 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; diff -r 0e2d57686b3c -r 943e2582dc87 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- /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;