# HG changeset patch # User wenzelm # Date 1243107067 -7200 # Node ID 2a1f5c87ac2884300f04a0a5841e90019de7f786 # Parent 67c796138bf077ddb71423fb894000666151d89c proper signature constraint; observe basic Isabelle/ML coding conventions, concerning parentheses, whitespace, indentation, and max. line length; diff -r 67c796138bf0 -r 2a1f5c87ac28 src/HOL/Tools/atp_minimal.ML --- a/src/HOL/Tools/atp_minimal.ML Sat May 23 17:39:19 2009 +0200 +++ b/src/HOL/Tools/atp_minimal.ML Sat May 23 21:31:07 2009 +0200 @@ -4,198 +4,217 @@ Minimalization of theorem list for metis by using an external automated theorem prover *) -structure AtpMinimal = +structure AtpMinimal: sig end = 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) +(* output control *) - 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 - in - fun split lst = isplit ([],[]) lst - end +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 - local - fun min p sup [] = raise Empty - | min p sup [s0] = [s0] - | min p sup s = - let - val (l0, r0) = split s - in - if p(sup @ l0) - then min p sup l0 - 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 - end +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 - (* return a minimal subset v of s that satisfies p - @pre p(s) & ~p([]) & monotone(p) - @post v subset s & p(v) & - forall e in v. ~p(v \ e) - *) - fun minimal p s = min p [] s + app (fn name => (debug (" " ^ name))) ordered end - (* failure check and producing answer*) - datatype 'a prove_result = Success of 'a | Failure | Timeout | Error - val string_of_result = fn - Success _ => "Success" - | Failure => "Failure" - | Timeout => "Timeout" - | Error => "Error" +(* minimalization algorithm *) - val failure_strings = - [("SPASS beiseite: Ran out of time.", Timeout), - ("Timeout", Timeout), - ("time limit exceeded", Timeout), - ("# Cannot determine problem status within resource limit", Timeout), - ("Error", Error)] +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 +in + fun split lst = isplit ([],[]) lst +end - fun produce_answer (success, message, result_string, thm_name_vec) = - if success then - (Success (Vector.foldr op:: [] thm_name_vec), result_string) - else +local + fun min p sup [] = raise Empty + | min p sup [s0] = [s0] + | min p sup s = let - val failure = get_first (fn (s, t) => if String.isSubstring s result_string then SOME (t, result_string) else NONE) failure_strings + val (l0, r0) = split s in - if is_some failure then - the failure + if p (sup @ l0) + then min p sup l0 else - (Failure, result_string) + 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 end +in + (* return a minimal subset v of s that satisfies p + @pre p(s) & ~p([]) & monotone(p) + @post v subset s & p(v) & + forall e in v. ~p(v \ e) + *) + fun minimal p s = min p [] s +end + - (* wrapper for calling external prover *) - fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs = +(* failure check and producing answer *) + +datatype 'a prove_result = Success of 'a | Failure | Timeout | Error + +val string_of_result = + fn Success _ => "Success" + | Failure => "Failure" + | Timeout => "Timeout" + | Error => "Error" + +val failure_strings = + [("SPASS beiseite: Ran out of time.", Timeout), + ("Timeout", Timeout), + ("time limit exceeded", Timeout), + ("# Cannot determine problem status within resource limit", Timeout), + ("Error", Error)] + +fun produce_answer (success, message, result_string, thm_name_vec) = + if success then + (Success (Vector.foldr op:: [] thm_name_vec), result_string) + else let - val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") - val name_thm_pairs = flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) 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 (result, proof) = - (produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state))) - val _ = println (string_of_result result) - val _ = debug proof + val failure = failure_strings |> get_first (fn (s, t) => + if String.isSubstring s result_string then SOME (t, result_string) else NONE) in - (result, proof) + if is_some failure then + the failure + else + (Failure, result_string) end - (* minimalization of thms *) - fun minimalize prover prover_name time_limit state name_thms_pairs = + +(* wrapper for calling external prover *) + +fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs = + let + val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") + val name_thm_pairs = + flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) 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 (result, proof) = + produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state)) + val _ = println (string_of_result result) + val _ = debug proof + in + (result, proof) + end + + +(* minimalization of thms *) + +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 t)) tl)) name_thms_pairs) + val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state + fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false + in + (* try prove first to check result and get used theorems *) + (case test_thms_fun name_thms_pairs of + (Success used, _) => + let + val ordered_used = order_unique 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 + else + name_thms_pairs + val min_thms = minimal test_thms to_use + val min_names = order_unique (map fst min_thms) + val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") + val _ = debug_fn (fn () => print_names min_thms) + in + answer ("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=...] ") + | (Error, msg) => + answer ("Error in prover: " ^ msg) + | (Failure, _) => + answer "Failure: No proof with the theorems supplied") + handle ResHolClause.TOO_TRIVIAL => + answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + | ERROR msg => + answer ("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 _ = 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 t)) tl)) name_thms_pairs) - val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state - fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false + val thmref = Facts.Named ((name, Position.none), interval) + val ths = ProofContext.get_fact context thmref + val name' = Facts.string_of_ref thmref in - (* try proove first to check result and get used theorems *) - (case test_thms_fun name_thms_pairs of - (Success used, _) => - let - val ordered_used = order_unique 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 - else - name_thms_pairs - val min_thms = (minimal test_thms to_use) - val min_names = order_unique (map fst min_thms) - val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") - val _ = debug_fn (fn () => print_names min_thms) - in - answer ("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=...] ") - | (Error, msg) => - answer ("Error in prover: " ^ msg) - | (Failure, _) => - answer "Failure: No proof with the theorems supplied") - handle ResHolClause.TOO_TRIVIAL => - answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") - | ERROR msg => - answer ("Error: " ^ msg) - end + (name', ths) + end) + +val default_prover = "remote_vampire" +val default_time_limit = 5 - (* 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) +fun get_time_limit_arg time_string = + (case Int.fromString time_string of + SOME t => t + | NONE => error ("Invalid time limit: " ^ quote time_string)) - 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)) - - val get_options = - let - val def = (default_prover, default_time_limit) - in - foldl (fn ((name, a), (p, t)) => (case name of +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 + end - fun sh_min_command args thm_names state = - let - val (prover_name, time_limit) = get_options args - val prover = - case AtpManager.get_prover prover_name (Proof.theory_of state) of - SOME prover => prover - | NONE => error ("Unknown prover: " ^ quote prover_name) - val name_thms_pairs = get_thms (Proof.context_of state) thm_names - in - minimalize prover prover_name time_limit state name_thms_pairs - end +fun sh_min_command args thm_names state = + let + val (prover_name, time_limit) = get_options args + val prover = + case AtpManager.get_prover prover_name (Proof.theory_of state) of + SOME prover => prover + | NONE => error ("Unknown prover: " ^ quote prover_name) + val name_thms_pairs = get_thms (Proof.context_of state) thm_names + in + 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) )) [] - val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) +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))) +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 +