1.1 --- a/src/HOL/Tools/atp_minimal.ML Tue Aug 04 16:13:16 2009 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,223 +0,0 @@
1.4 -(* Title: HOL/Tools/atp_minimal.ML
1.5 - Author: Philipp Meyer, TU Muenchen
1.6 -
1.7 -Minimalization of theorem list for metis by using an external automated theorem prover
1.8 -*)
1.9 -
1.10 -structure AtpMinimal: sig end =
1.11 -struct
1.12 -
1.13 -(* output control *)
1.14 -
1.15 -fun debug str = Output.debug (fn () => str)
1.16 -fun debug_fn f = if ! Output.debugging then f () else ()
1.17 -fun answer str = Output.writeln str
1.18 -fun println str = Output.priority str
1.19 -
1.20 -fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
1.21 -fun length_string namelist = Int.toString (length namelist)
1.22 -
1.23 -fun print_names name_thms_pairs =
1.24 - let
1.25 - val names = map fst name_thms_pairs
1.26 - val ordered = order_unique names
1.27 - in
1.28 - app (fn name => (debug (" " ^ name))) ordered
1.29 - end
1.30 -
1.31 -
1.32 -(* minimalization algorithm *)
1.33 -
1.34 -local
1.35 - fun isplit (l,r) [] = (l,r)
1.36 - | isplit (l,r) (h::[]) = (h::l, r)
1.37 - | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
1.38 -in
1.39 - fun split lst = isplit ([],[]) lst
1.40 -end
1.41 -
1.42 -local
1.43 - fun min p sup [] = raise Empty
1.44 - | min p sup [s0] = [s0]
1.45 - | min p sup s =
1.46 - let
1.47 - val (l0, r0) = split s
1.48 - in
1.49 - if p (sup @ l0)
1.50 - then min p sup l0
1.51 - else
1.52 - if p (sup @ r0)
1.53 - then min p sup r0
1.54 - else
1.55 - let
1.56 - val l = min p (sup @ r0) l0
1.57 - val r = min p (sup @ l) r0
1.58 - in
1.59 - l @ r
1.60 - end
1.61 - end
1.62 -in
1.63 - (* return a minimal subset v of s that satisfies p
1.64 - @pre p(s) & ~p([]) & monotone(p)
1.65 - @post v subset s & p(v) &
1.66 - forall e in v. ~p(v \ e)
1.67 - *)
1.68 - fun minimal p s = min p [] s
1.69 -end
1.70 -
1.71 -
1.72 -(* failure check and producing answer *)
1.73 -
1.74 -datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
1.75 -
1.76 -val string_of_result =
1.77 - fn Success _ => "Success"
1.78 - | Failure => "Failure"
1.79 - | Timeout => "Timeout"
1.80 - | Error => "Error"
1.81 -
1.82 -val failure_strings =
1.83 - [("SPASS beiseite: Ran out of time.", Timeout),
1.84 - ("Timeout", Timeout),
1.85 - ("time limit exceeded", Timeout),
1.86 - ("# Cannot determine problem status within resource limit", Timeout),
1.87 - ("Error", Error)]
1.88 -
1.89 -fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
1.90 - if success then
1.91 - (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
1.92 - else
1.93 - let
1.94 - val failure = failure_strings |> get_first (fn (s, t) =>
1.95 - if String.isSubstring s result_string then SOME (t, result_string) else NONE)
1.96 - in
1.97 - if is_some failure then
1.98 - the failure
1.99 - else
1.100 - (Failure, result_string)
1.101 - end
1.102 -
1.103 -
1.104 -(* wrapper for calling external prover *)
1.105 -
1.106 -fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
1.107 - let
1.108 - val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
1.109 - val name_thm_pairs =
1.110 - flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
1.111 - val _ = debug_fn (fn () => print_names name_thm_pairs)
1.112 - val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
1.113 - val (result, proof) =
1.114 - produce_answer
1.115 - (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
1.116 - val _ = println (string_of_result result)
1.117 - val _ = debug proof
1.118 - in
1.119 - (result, proof)
1.120 - end
1.121 -
1.122 -
1.123 -(* minimalization of thms *)
1.124 -
1.125 -fun minimalize prover prover_name time_limit state name_thms_pairs =
1.126 - let
1.127 - val _ =
1.128 - println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
1.129 - ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
1.130 - val _ = debug_fn (fn () => app (fn (n, tl) =>
1.131 - (debug n; app (fn t =>
1.132 - debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
1.133 - val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
1.134 - fun test_thms filtered thms =
1.135 - case test_thms_fun filtered thms of (Success _, _) => true | _ => false
1.136 - in
1.137 - (* try prove first to check result and get used theorems *)
1.138 - (case test_thms_fun NONE name_thms_pairs of
1.139 - (Success (used, filtered), _) =>
1.140 - let
1.141 - val ordered_used = order_unique used
1.142 - val to_use =
1.143 - if length ordered_used < length name_thms_pairs then
1.144 - filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
1.145 - else
1.146 - name_thms_pairs
1.147 - val min_thms = (minimal (test_thms (SOME filtered)) to_use)
1.148 - val min_names = order_unique (map fst min_thms)
1.149 - val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
1.150 - val _ = debug_fn (fn () => print_names min_thms)
1.151 - in
1.152 - answer ("Try this command: " ^
1.153 - Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
1.154 - end
1.155 - | (Timeout, _) =>
1.156 - answer ("Timeout: You may need to increase the time limit of " ^
1.157 - Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
1.158 - | (Error, msg) =>
1.159 - answer ("Error in prover: " ^ msg)
1.160 - | (Failure, _) =>
1.161 - answer "Failure: No proof with the theorems supplied")
1.162 - handle ResHolClause.TOO_TRIVIAL =>
1.163 - answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
1.164 - | ERROR msg =>
1.165 - answer ("Error: " ^ msg)
1.166 - end
1.167 -
1.168 -
1.169 -(* Isar command and parsing input *)
1.170 -
1.171 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
1.172 -
1.173 -fun get_thms context =
1.174 - map (fn (name, interval) =>
1.175 - let
1.176 - val thmref = Facts.Named ((name, Position.none), interval)
1.177 - val ths = ProofContext.get_fact context thmref
1.178 - val name' = Facts.string_of_ref thmref
1.179 - in
1.180 - (name', ths)
1.181 - end)
1.182 -
1.183 -val default_prover = "remote_vampire"
1.184 -val default_time_limit = 5
1.185 -
1.186 -fun get_time_limit_arg time_string =
1.187 - (case Int.fromString time_string of
1.188 - SOME t => t
1.189 - | NONE => error ("Invalid time limit: " ^ quote time_string))
1.190 -
1.191 -val get_options =
1.192 - let
1.193 - val def = (default_prover, default_time_limit)
1.194 - in
1.195 - foldl (fn ((name, a), (p, t)) =>
1.196 - (case name of
1.197 - "time" => (p, (get_time_limit_arg a))
1.198 - | "atp" => (a, t)
1.199 - | n => error ("Invalid argument: " ^ n))) def
1.200 - end
1.201 -
1.202 -fun sh_min_command args thm_names state =
1.203 - let
1.204 - val (prover_name, time_limit) = get_options args
1.205 - val prover =
1.206 - case AtpManager.get_prover prover_name (Proof.theory_of state) of
1.207 - SOME prover => prover
1.208 - | NONE => error ("Unknown prover: " ^ quote prover_name)
1.209 - val name_thms_pairs = get_thms (Proof.context_of state) thm_names
1.210 - in
1.211 - minimalize prover prover_name time_limit state name_thms_pairs
1.212 - end
1.213 -
1.214 -val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
1.215 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
1.216 -
1.217 -val _ =
1.218 - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
1.219 - (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
1.220 - Toplevel.no_timing o Toplevel.unknown_proof o
1.221 - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
1.222 -
1.223 -end
1.224 -
1.225 -end
1.226 -