# HG changeset patch # User blanchet # Date 1269007664 -3600 # Node ID 513074557e0609a3172ea1439931a6aeef4d5f0e # Parent 2f8fb5242799288365f4f576a0933a050d4e534d move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later diff -r 2f8fb5242799 -r 513074557e06 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Mar 19 15:07:44 2010 +0100 @@ -320,6 +320,7 @@ Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \ Tools/Sledgehammer/sledgehammer_fol_clause.ML \ Tools/Sledgehammer/sledgehammer_hol_clause.ML \ + Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ Tools/string_code.ML \ Tools/string_syntax.ML \ diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:07:44 2010 +0100 @@ -42,8 +42,7 @@ datatype min_data = MinData of { succs: int, - ab_ratios: int, - it_ratios: int + ab_ratios: int } fun make_sh_data @@ -51,8 +50,8 @@ ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail} -fun make_min_data (succs, ab_ratios, it_ratios) = - MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios} +fun make_min_data (succs, ab_ratios) = + MinData{succs=succs, ab_ratios=ab_ratios} fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) = MeData{calls=calls, success=success, proofs=proofs, time=time, @@ -66,8 +65,7 @@ time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) = - (succs, ab_ratios, it_ratios) +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas, posns}) = (calls, success, proofs, time, timeout, lemmas, posns) @@ -147,13 +145,10 @@ => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t)) val inc_min_succs = map_min_data - (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios)) + (fn (succs,ab_ratios) => (succs+1, ab_ratios)) fun inc_min_ab_ratios r = map_min_data - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios)) - -fun inc_min_it_ratios r = map_min_data - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) + (fn (succs, ab_ratios) => (succs, ab_ratios+r)) val inc_metis_calls = map_me_data (fn (calls,success,proofs,time,timeout,lemmas,posns) @@ -234,10 +229,9 @@ else () ) -fun log_min_data log (succs, ab_ratios, it_ratios) = +fun log_min_data log (succs, ab_ratios) = (log ("Number of successful minimizations: " ^ string_of_int succs); - log ("After/before ratios: " ^ string_of_int ab_ratios); - log ("Iterations ratios: " ^ string_of_int it_ratios) + log ("After/before ratios: " ^ string_of_int ab_ratios) ) in @@ -380,9 +374,10 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let + open ATP_Minimal val n0 = length (these (!named_thms)) val (prover_name, prover) = get_atp (Proof.theory_of st) args - val minimize = ATP_Minimal.minimalize prover prover_name + val minimize = minimize_theorems linear_minimize prover prover_name val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) @@ -393,7 +388,6 @@ (SOME (named_thms',its), msg) => (change_data id inc_min_succs; change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); - change_data id (inc_min_it_ratios ((100*its) div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") else (named_thms := SOME named_thms'; diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 15:07:44 2010 +0100 @@ -20,6 +20,7 @@ ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_wrapper.ML") ("Tools/ATP_Manager/atp_minimal.ML") + ("Tools/Sledgehammer/sledgehammer_isar.ML") ("Tools/Sledgehammer/meson_tactic.ML") ("Tools/Sledgehammer/metis_tactics.ML") begin @@ -90,6 +91,7 @@ apply (simp add: COMBC_def) done + subsection {* Setup of external ATPs *} use "Tools/Sledgehammer/sledgehammer_fol_clause.ML" @@ -122,6 +124,8 @@ setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} +use "Tools/Sledgehammer/sledgehammer_isar.ML" + subsection {* The MESON prover *} diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:07:44 2010 +0100 @@ -282,36 +282,4 @@ val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers; in () end; - - -(** Isar command syntax **) - -local structure K = OuterKeyword and P = OuterParse in - -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.command "sledgehammer" "call all 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))); - end; - -end; - diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:07:44 2010 +0100 @@ -6,27 +6,31 @@ signature ATP_MINIMAL = sig - val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state -> - (string * thm list) list -> ((string * thm list) list * int) option * string - (* To be removed once TN has finished his measurements; - the int component of the result should then be removed: *) - val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> - (string * thm list) list -> ((string * thm list) list * int) option * string -end + type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list + val linear_minimize : 'a minimize_fun + val binary_minimize : 'a minimize_fun + val minimize_theorems : + (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int + -> Proof.state -> (string * thm list) list + -> (string * thm list) list option * string +end; structure ATP_Minimal : ATP_MINIMAL = struct -(* Linear minimization *) +open Sledgehammer_Fact_Preprocessor + +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list + +(* Linear minimization algorithm *) -fun lin_gen_minimize p s = -let - fun min [] needed = needed - | min (x::xs) needed = - if p(xs @ needed) then min xs needed else min xs (x::needed) -in (min s [], length s) end; +fun linear_minimize p s = + let + fun aux [] needed = needed + | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x) + in aux s [] end; -(* Clever minimalization algorithm *) +(* Binary minimalization *) local fun isplit (l, r) [] = (l, r) @@ -37,24 +41,21 @@ end local - fun min p sup [] = raise Empty - | min p sup [s0] = [s0] + fun min _ _ [] = raise Empty + | min _ _ [s0] = [s0] | min p sup s = let val (l0, r0) = split s in - if p (sup @ l0) - then min p sup l0 + if p (sup @ l0) then + min p sup l0 + else if p (sup @ r0) then + min p sup r0 else - if p (sup @ r0) - then min p sup r0 - else - let - val l = min p (sup @ r0) l0 - val r = min p (sup @ l) r0 - in - l @ r - end + let + val l = min p (sup @ r0) l0 + val r = min p (sup @ l) r0 + in l @ r end end in (* return a minimal subset v of s that satisfies p @@ -62,15 +63,10 @@ @post v subset s & p(v) & forall e in v. ~p(v \ e) *) - fun minimal p s = - let - val count = Unsynchronized.ref 0 - fun p_count xs = (Unsynchronized.inc count; p xs) - val v = - (case min p_count [] s of - [x] => if p_count [] then [] else [x] - | m => m); - in (v, ! count) end + fun binary_minimize p s = + case min p [] s of + [x] => if p [] then [] else [x] + | m => m end @@ -91,7 +87,7 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer (result: ATP_Wrapper.prover_result) = +fun produce_answer (result : ATP_Wrapper.prover_result) = let val {success, proof = result_string, internal_thm_names = thm_name_vec, filtered_clauses = filtered, ...} = result @@ -116,7 +112,7 @@ let val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {with_full_types = ! ATP_Manager.full_types, @@ -133,7 +129,8 @@ (* minimalization of thms *) -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs = +fun minimize_theorems gen_min prover prover_name time_limit state + name_thms_pairs = let val _ = priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ @@ -152,15 +149,14 @@ if length ordered_used < length name_thms_pairs then filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val (min_thms, n) = - if null to_use then ([], 0) + val min_thms = + if null to_use then [] else gen_min (test_thms (SOME filtered)) to_use val min_names = sort_distinct string_ord (map fst min_thms) val _ = priority (cat_lines - ["Iterations: " ^ string_of_int n (* FIXME TN remove later *), - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) + ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in - (SOME (min_thms, n), "Try this command: " ^ + (SOME min_thms, "Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) end | (Timeout, _) => @@ -171,67 +167,8 @@ | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => (NONE, "Error: " ^ msg) end - -(* Isar command and parsing input *) - -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in - -fun get_thms context = - map (fn (name, interval) => - let - val thmref = Facts.Named ((name, Position.none), interval) - val ths = ProofContext.get_fact context thmref - val name' = Facts.string_of_ref thmref - in - (name', ths) - end) - -val default_prover = "remote_vampire" -val default_time_limit = 5 - -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_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_prover, default_time_limit) - -val minimize = gen_minimalize lin_gen_minimize - -val minimalize = gen_minimalize minimal - -fun sh_min_command args thm_names state = - let - val (prover_name, time_limit) = get_options args - val prover = - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of - SOME prover => prover - | NONE => error ("Unknown prover: " ^ quote prover_name)) - val name_thms_pairs = get_thms (Proof.context_of state) thm_names - in - writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs)) - end - -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.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 (sh_min_command args thm_names o Toplevel.proof_of))) - -end - -end +end; diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 19 15:07:44 2010 +0100 @@ -13,7 +13,7 @@ val auto: bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params val setup : theory -> theory -end +end; structure Nitpick_Isar : NITPICK_ISAR = struct diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 19 15:07:44 2010 +0100 @@ -12,7 +12,7 @@ hol_context -> (typ option * bool option) list -> (typ option * bool option) list -> term -> term list * term list * bool * bool * bool -end +end; structure Nitpick_Preproc : NITPICK_PREPROC = struct diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 19 15:07:44 2010 +0100 @@ -8,7 +8,7 @@ signature NITPICK_TESTS = sig val run_all_tests : unit -> unit -end +end; structure Nitpick_Tests = struct diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Mar 19 13:02:18 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Mar 19 15:07:44 2010 +0100 @@ -62,7 +62,7 @@ val pstrs : string -> Pretty.T list val unyxml : string -> string val maybe_quote : string -> string -end +end; structure Nitpick_Util : NITPICK_UTIL = struct diff -r 2f8fb5242799 -r 513074557e06 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 19 15:07:44 2010 +0100 @@ -0,0 +1,87 @@ +(* Title: HOL/Sledgehammer/sledgehammer_isar.ML + Author: Jasmin Blanchette, TU Muenchen + +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. +*) + +structure Sledgehammer_Isar : sig end = +struct + +open ATP_Manager +open ATP_Minimal + +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)); + +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.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))); + +val default_minimize_prover = "remote_vampire" +val default_minimize_time_limit = 5 + +fun atp_minimize_command args thm_names state = + let + fun theorems_from_names ctxt = + map (fn (name, interval) => + let + val thmref = Facts.Named ((name, Position.none), interval) + 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_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 prover = + (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of + SOME prover => prover + | NONE => error ("Unknown prover: " ^ quote prover_name)) + val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names + in + writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit + 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.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 + +end;