--- 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
+