1.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:07:44 2010 +0100
1.3 @@ -6,27 +6,31 @@
1.4
1.5 signature ATP_MINIMAL =
1.6 sig
1.7 - val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
1.8 - (string * thm list) list -> ((string * thm list) list * int) option * string
1.9 - (* To be removed once TN has finished his measurements;
1.10 - the int component of the result should then be removed: *)
1.11 - val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
1.12 - (string * thm list) list -> ((string * thm list) list * int) option * string
1.13 -end
1.14 + type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
1.15 + val linear_minimize : 'a minimize_fun
1.16 + val binary_minimize : 'a minimize_fun
1.17 + val minimize_theorems :
1.18 + (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
1.19 + -> Proof.state -> (string * thm list) list
1.20 + -> (string * thm list) list option * string
1.21 +end;
1.22
1.23 structure ATP_Minimal : ATP_MINIMAL =
1.24 struct
1.25
1.26 -(* Linear minimization *)
1.27 +open Sledgehammer_Fact_Preprocessor
1.28
1.29 -fun lin_gen_minimize p s =
1.30 -let
1.31 - fun min [] needed = needed
1.32 - | min (x::xs) needed =
1.33 - if p(xs @ needed) then min xs needed else min xs (x::needed)
1.34 -in (min s [], length s) end;
1.35 +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
1.36
1.37 -(* Clever minimalization algorithm *)
1.38 +(* Linear minimization algorithm *)
1.39 +
1.40 +fun linear_minimize p s =
1.41 + let
1.42 + fun aux [] needed = needed
1.43 + | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
1.44 + in aux s [] end;
1.45 +
1.46 +(* Binary minimalization *)
1.47
1.48 local
1.49 fun isplit (l, r) [] = (l, r)
1.50 @@ -37,24 +41,21 @@
1.51 end
1.52
1.53 local
1.54 - fun min p sup [] = raise Empty
1.55 - | min p sup [s0] = [s0]
1.56 + fun min _ _ [] = raise Empty
1.57 + | min _ _ [s0] = [s0]
1.58 | min p sup s =
1.59 let
1.60 val (l0, r0) = split s
1.61 in
1.62 - if p (sup @ l0)
1.63 - then min p sup l0
1.64 + if p (sup @ l0) then
1.65 + min p sup l0
1.66 + else if p (sup @ r0) then
1.67 + min p sup r0
1.68 else
1.69 - if p (sup @ r0)
1.70 - then min p sup r0
1.71 - else
1.72 - let
1.73 - val l = min p (sup @ r0) l0
1.74 - val r = min p (sup @ l) r0
1.75 - in
1.76 - l @ r
1.77 - end
1.78 + let
1.79 + val l = min p (sup @ r0) l0
1.80 + val r = min p (sup @ l) r0
1.81 + in l @ r end
1.82 end
1.83 in
1.84 (* return a minimal subset v of s that satisfies p
1.85 @@ -62,15 +63,10 @@
1.86 @post v subset s & p(v) &
1.87 forall e in v. ~p(v \ e)
1.88 *)
1.89 - fun minimal p s =
1.90 - let
1.91 - val count = Unsynchronized.ref 0
1.92 - fun p_count xs = (Unsynchronized.inc count; p xs)
1.93 - val v =
1.94 - (case min p_count [] s of
1.95 - [x] => if p_count [] then [] else [x]
1.96 - | m => m);
1.97 - in (v, ! count) end
1.98 + fun binary_minimize p s =
1.99 + case min p [] s of
1.100 + [x] => if p [] then [] else [x]
1.101 + | m => m
1.102 end
1.103
1.104
1.105 @@ -91,7 +87,7 @@
1.106 ("# Cannot determine problem status within resource limit", Timeout),
1.107 ("Error", Error)]
1.108
1.109 -fun produce_answer (result: ATP_Wrapper.prover_result) =
1.110 +fun produce_answer (result : ATP_Wrapper.prover_result) =
1.111 let
1.112 val {success, proof = result_string, internal_thm_names = thm_name_vec,
1.113 filtered_clauses = filtered, ...} = result
1.114 @@ -116,7 +112,7 @@
1.115 let
1.116 val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
1.117 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
1.118 - val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
1.119 + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
1.120 val {context = ctxt, facts, goal} = Proof.goal state
1.121 val problem =
1.122 {with_full_types = ! ATP_Manager.full_types,
1.123 @@ -133,7 +129,8 @@
1.124
1.125 (* minimalization of thms *)
1.126
1.127 -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
1.128 +fun minimize_theorems gen_min prover prover_name time_limit state
1.129 + name_thms_pairs =
1.130 let
1.131 val _ =
1.132 priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
1.133 @@ -152,15 +149,14 @@
1.134 if length ordered_used < length name_thms_pairs then
1.135 filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
1.136 else name_thms_pairs
1.137 - val (min_thms, n) =
1.138 - if null to_use then ([], 0)
1.139 + val min_thms =
1.140 + if null to_use then []
1.141 else gen_min (test_thms (SOME filtered)) to_use
1.142 val min_names = sort_distinct string_ord (map fst min_thms)
1.143 val _ = priority (cat_lines
1.144 - ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
1.145 - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
1.146 + ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
1.147 in
1.148 - (SOME (min_thms, n), "Try this command: " ^
1.149 + (SOME min_thms, "Try this command: " ^
1.150 Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
1.151 end
1.152 | (Timeout, _) =>
1.153 @@ -171,67 +167,8 @@
1.154 | (Failure, _) =>
1.155 (NONE, "Failure: No proof with the theorems supplied"))
1.156 handle Sledgehammer_HOL_Clause.TRIVIAL =>
1.157 - (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
1.158 + (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
1.159 | ERROR msg => (NONE, "Error: " ^ msg)
1.160 end
1.161
1.162 -
1.163 -(* Isar command and parsing input *)
1.164 -
1.165 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
1.166 -
1.167 -fun get_thms context =
1.168 - map (fn (name, interval) =>
1.169 - let
1.170 - val thmref = Facts.Named ((name, Position.none), interval)
1.171 - val ths = ProofContext.get_fact context thmref
1.172 - val name' = Facts.string_of_ref thmref
1.173 - in
1.174 - (name', ths)
1.175 - end)
1.176 -
1.177 -val default_prover = "remote_vampire"
1.178 -val default_time_limit = 5
1.179 -
1.180 -fun get_time_limit_arg time_string =
1.181 - (case Int.fromString time_string of
1.182 - SOME t => t
1.183 - | NONE => error ("Invalid time limit: " ^ quote time_string))
1.184 -
1.185 -fun get_opt (name, a) (p, t) =
1.186 - (case name of
1.187 - "time" => (p, get_time_limit_arg a)
1.188 - | "atp" => (a, t)
1.189 - | n => error ("Invalid argument: " ^ n))
1.190 -
1.191 -fun get_options args = fold get_opt args (default_prover, default_time_limit)
1.192 -
1.193 -val minimize = gen_minimalize lin_gen_minimize
1.194 -
1.195 -val minimalize = gen_minimalize minimal
1.196 -
1.197 -fun sh_min_command args thm_names state =
1.198 - let
1.199 - val (prover_name, time_limit) = get_options args
1.200 - val prover =
1.201 - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
1.202 - SOME prover => prover
1.203 - | NONE => error ("Unknown prover: " ^ quote prover_name))
1.204 - val name_thms_pairs = get_thms (Proof.context_of state) thm_names
1.205 - in
1.206 - writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
1.207 - end
1.208 -
1.209 -val parse_args =
1.210 - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
1.211 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
1.212 -
1.213 -val _ =
1.214 - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
1.215 - (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
1.216 - Toplevel.no_timing o Toplevel.unknown_proof o
1.217 - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
1.218 -
1.219 -end
1.220 -
1.221 -end
1.222 +end;