# HG changeset patch # User wenzelm # Date 1255619179 -7200 # Node ID 3c19b98a35cd04c1008966da72ee3b5299fdcb4f # Parent 22664da2923b3494a87a9944c49064a15c015cb5 ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification; diff -r 22664da2923b -r 3c19b98a35cd src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 17:04:45 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 17:06:19 2009 +0200 @@ -287,7 +287,7 @@ fun get_atp thy args = AList.lookup (op =) args proverK |> the_default (hd (ATP_Manager.get_atps ())) (* FIXME partial *) - |> (fn name => (name, the (ATP_Manager.get_prover name thy))) (* FIXME partial *) + |> (fn name => (name, the (ATP_Manager.get_prover thy name))) (* FIXME partial *) local diff -r 22664da2923b -r 3c19b98a35cd src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 17:04:45 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 17:06:19 2009 +0200 @@ -20,7 +20,7 @@ val messages: int option -> unit val add_prover: string * ATP_Wrapper.prover -> theory -> theory val print_provers: theory -> unit - val get_prover: string -> theory -> ATP_Wrapper.prover option + val get_prover: theory -> string -> ATP_Wrapper.prover option val sledgehammer: string list -> Proof.state -> unit end; @@ -302,7 +302,7 @@ fun print_provers thy = Pretty.writeln (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy)))); -fun get_prover name thy = +fun get_prover thy name = (case Symtab.lookup (Provers.get thy) name of NONE => NONE | SOME (prover, _) => SOME prover); @@ -311,7 +311,7 @@ (* start prover thread *) fun start_prover name birthtime deadtime i proof_state = - (case get_prover name (Proof.theory_of proof_state) of + (case get_prover (Proof.theory_of proof_state) name of NONE => warning ("Unknown external prover: " ^ quote name) | SOME prover => let diff -r 22664da2923b -r 3c19b98a35cd src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 17:04:45 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 17:06:19 2009 +0200 @@ -13,33 +13,14 @@ structure ATP_Minimal: ATP_MINIMAL = struct -(* output control *) - -fun debug str = Output.debug (fn () => str) -fun debug_fn f = if ! Output.debugging then f () else () -fun answer str = Output.writeln str -fun println str = Output.priority str - -fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list -fun length_string namelist = Int.toString (length namelist) - -fun print_names name_thms_pairs = - let - val names = map fst name_thms_pairs - val ordered = order_unique names - in - app (fn name => (debug (" " ^ name))) ordered - end - - (* minimalization algorithm *) local - fun isplit (l,r) [] = (l,r) - | isplit (l,r) (h::[]) = (h::l, r) - | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t + fun isplit (l, r) [] = (l, r) + | isplit (l, r) [h] = (h :: l, r) + | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t in - fun split lst = isplit ([],[]) lst + fun split lst = isplit ([], []) lst end local @@ -69,14 +50,14 @@ forall e in v. ~p(v \ e) *) fun minimal p s = - let val c = Unsynchronized.ref 0 - fun pc xs = (c := !c + 1; p xs) - in - (case min pc [] s of - [x] => if pc [] then [] else [x] - | m => m, - !c) - end + 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 end @@ -102,18 +83,17 @@ val {success, proof = result_string, internal_thm_names = thm_name_vec, filtered_clauses = filtered, ...} = result in - if success then - (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) - else - let - val failure = failure_strings |> get_first (fn (s, t) => - if String.isSubstring s result_string then SOME (t, result_string) else NONE) - in - if is_some failure then - the failure - else - (Failure, result_string) - end + if success then + (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string) + else + let + val failure = failure_strings |> get_first (fn (s, t) => + if String.isSubstring s result_string then SOME (t, result_string) else NONE) + in + (case failure of + SOME res => res + | NONE => (Failure, result_string)) + end end @@ -121,9 +101,8 @@ fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = let - val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") + 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 _ = debug_fn (fn () => print_names name_thm_pairs) val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val problem = {with_full_types = ! ATP_Manager.full_types, @@ -132,8 +111,7 @@ axiom_clauses = SOME axclauses, filtered_clauses = filtered} val (result, proof) = produce_answer (prover problem time_limit) - val _ = println (string_of_result result) - val _ = debug proof + val _ = priority (string_of_result result) in (result, proof) end @@ -144,21 +122,18 @@ fun minimalize prover prover_name time_limit state name_thms_pairs = let val _ = - println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: " - ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds") - val _ = debug_fn (fn () => app (fn (n, tl) => - (debug n; app (fn t => - debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs) + priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ + " theorems, prover: " ^ prover_name ^ + ", time limit: " ^ string_of_int time_limit ^ " seconds") val test_thms_fun = sh_test_thms prover time_limit 1 state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false - val answer' = pair and answer'' = pair NONE in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of (Success (used, filtered), _) => let - val ordered_used = order_unique used + val ordered_used = sort_distinct string_ord used val to_use = if length ordered_used < length name_thms_pairs then filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs @@ -166,25 +141,24 @@ name_thms_pairs val (min_thms, n) = if null to_use then ([], 0) else minimal (test_thms (SOME filtered)) to_use - val min_names = order_unique (map fst min_thms) - val _ = println ("Interations: " ^ string_of_int n) - val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") - val _ = debug_fn (fn () => print_names min_thms) + val min_names = sort_distinct string_ord (map fst min_thms) + val _ = priority (cat_lines + ["Interations: " ^ string_of_int n, + "Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in - answer' (SOME(min_thms,n)) ("Try this command: " ^ + (SOME (min_thms, n), "Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) end | (Timeout, _) => - answer'' ("Timeout: You may need to increase the time limit of " ^ - Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ") + (NONE, "Timeout: You may need to increase the time limit of " ^ + string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ") | (Error, msg) => - answer'' ("Error in prover: " ^ msg) + (NONE, "Error in prover: " ^ msg) | (Failure, _) => - answer'' "Failure: No proof with the theorems supplied") + (NONE, "Failure: No proof with the theorems supplied")) handle ResHolClause.TOO_TRIVIAL => - answer' (SOME ([],0)) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") - | ERROR msg => - answer'' ("Error: " ^ msg) + (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + | ERROR msg => (NONE, "Error: " ^ msg) end @@ -210,28 +184,24 @@ SOME t => t | NONE => error ("Invalid time limit: " ^ quote time_string)) -val get_options = - let - val def = (default_prover, default_time_limit) - in - foldl (fn ((name, a), (p, t)) => - (case name of - "time" => (p, (get_time_limit_arg a)) - | "atp" => (a, t) - | n => error ("Invalid argument: " ^ n))) def - end +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) fun sh_min_command args thm_names state = let val (prover_name, time_limit) = get_options args val prover = - case ATP_Manager.get_prover prover_name (Proof.theory_of state) of + (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of SOME prover => prover - | NONE => error ("Unknown prover: " ^ quote prover_name) + | NONE => error ("Unknown prover: " ^ quote prover_name)) val name_thms_pairs = get_thms (Proof.context_of state) thm_names - fun print_answer (_, msg) = answer msg in - print_answer (minimalize prover prover_name time_limit state name_thms_pairs) + writeln (#2 (minimalize prover prover_name time_limit state name_thms_pairs)) end val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []