1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -18,6 +18,11 @@
1.4 val mepoN : string
1.5 val mashN : string
1.6 val meshN : string
1.7 + val unlearnN : string
1.8 + val learn_isarN : string
1.9 + val learn_atpN : string
1.10 + val relearn_isarN : string
1.11 + val relearn_atpN : string
1.12 val fact_filters : string list
1.13 val escape_meta : string -> string
1.14 val escape_metas : string list -> string
1.15 @@ -31,12 +36,15 @@
1.16 val is_likely_tautology_or_too_meta : thm -> bool
1.17 val theory_ord : theory * theory -> order
1.18 val thm_ord : thm * thm -> order
1.19 - val features_of :
1.20 - Proof.context -> string -> theory -> stature -> term list -> string list
1.21 - val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
1.22 val goal_of_thm : theory -> thm -> thm
1.23 val run_prover_for_mash :
1.24 Proof.context -> params -> string -> fact list -> thm -> prover_result
1.25 + val features_of :
1.26 + Proof.context -> string -> theory -> stature -> term list -> string list
1.27 + val isar_dependencies_of : unit Symtab.table -> thm -> string list
1.28 + val atp_dependencies_of :
1.29 + Proof.context -> params -> string -> bool -> fact list -> unit Symtab.table
1.30 + -> thm -> string list
1.31 val mash_CLEAR : Proof.context -> unit
1.32 val mash_ADD :
1.33 Proof.context -> bool
1.34 @@ -53,8 +61,9 @@
1.35 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
1.36 -> unit
1.37 val mash_learn_facts :
1.38 - Proof.context -> params -> Time.time -> fact list -> string
1.39 - val mash_learn : Proof.context -> params -> unit
1.40 + Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
1.41 + -> string
1.42 + val mash_learn : Proof.context -> params -> bool -> unit
1.43 val relevant_facts :
1.44 Proof.context -> params -> string -> int -> fact_override -> term list
1.45 -> term -> fact list -> fact list
1.46 @@ -85,6 +94,12 @@
1.47
1.48 val fact_filters = [meshN, mepoN, mashN]
1.49
1.50 +val unlearnN = "unlearn"
1.51 +val learn_isarN = "learn_isar"
1.52 +val learn_atpN = "learn_atp"
1.53 +val relearn_isarN = "relearn_isar"
1.54 +val relearn_atpN = "relearn_atp"
1.55 +
1.56 fun mash_home () = getenv "MASH_HOME"
1.57 fun mash_state_dir () =
1.58 getenv "ISABELLE_HOME_USER" ^ "/mash"
1.59 @@ -212,6 +227,28 @@
1.60
1.61 val thm_ord = theory_ord o pairself theory_of_thm
1.62
1.63 +val freezeT = Type.legacy_freeze_type
1.64 +
1.65 +fun freeze (t $ u) = freeze t $ freeze u
1.66 + | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
1.67 + | freeze (Var ((s, _), T)) = Free (s, freezeT T)
1.68 + | freeze (Const (s, T)) = Const (s, freezeT T)
1.69 + | freeze (Free (s, T)) = Free (s, freezeT T)
1.70 + | freeze t = t
1.71 +
1.72 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
1.73 +
1.74 +fun run_prover_for_mash ctxt params prover facts goal =
1.75 + let
1.76 + val problem =
1.77 + {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
1.78 + facts = facts |> map (apfst (apfst (fn name => name ())))
1.79 + |> map Untranslated_Fact}
1.80 + in
1.81 + get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K "")))
1.82 + problem
1.83 + end
1.84 +
1.85 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
1.86
1.87 fun interesting_terms_types_and_classes ctxt prover term_max_depth
1.88 @@ -277,27 +314,57 @@
1.89 | Simp => cons "simp"
1.90 | Def => cons "def")
1.91
1.92 -fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
1.93 +fun isar_dependencies_of all_facts = thms_in_proof (SOME all_facts)
1.94
1.95 -val freezeT = Type.legacy_freeze_type
1.96 +val atp_dep_default_max_fact = 50
1.97
1.98 -fun freeze (t $ u) = freeze t $ freeze u
1.99 - | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
1.100 - | freeze (Var ((s, _), T)) = Free (s, freezeT T)
1.101 - | freeze (Const (s, T)) = Const (s, freezeT T)
1.102 - | freeze (Free (s, T)) = Free (s, freezeT T)
1.103 - | freeze t = t
1.104 -
1.105 -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
1.106 -
1.107 -fun run_prover_for_mash ctxt params prover facts goal =
1.108 - let
1.109 - val problem =
1.110 - {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
1.111 - facts = facts |> map (apfst (apfst (fn name => name ())))
1.112 - |> map Untranslated_Fact}
1.113 - val prover = get_minimizing_prover ctxt Normal (K ()) prover
1.114 - in prover params (K (K (K ""))) problem end
1.115 +fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto
1.116 + facts all_names th =
1.117 + case isar_dependencies_of all_names th of
1.118 + [] => []
1.119 + | isar_deps =>
1.120 + let
1.121 + val thy = Proof_Context.theory_of ctxt
1.122 + val goal = goal_of_thm thy th
1.123 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
1.124 + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
1.125 + fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
1.126 + fun is_dep dep (_, th) = nickname_of th = dep
1.127 + fun add_isar_dep facts dep accum =
1.128 + if exists (is_dep dep) accum then
1.129 + accum
1.130 + else case find_first (is_dep dep) facts of
1.131 + SOME ((name, status), th) => accum @ [((name, status), th)]
1.132 + | NONE => accum (* shouldn't happen *)
1.133 + val facts =
1.134 + facts |> iterative_relevant_facts ctxt params prover
1.135 + (max_facts |> the_default atp_dep_default_max_fact) NONE
1.136 + hyp_ts concl_t
1.137 + |> fold (add_isar_dep facts) isar_deps
1.138 + |> map fix_name
1.139 + in
1.140 + if verbose andalso not auto then
1.141 + let val num_facts = length facts in
1.142 + "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
1.143 + " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
1.144 + "."
1.145 + |> Output.urgent_message
1.146 + end
1.147 + else
1.148 + ();
1.149 + case run_prover_for_mash ctxt params prover facts goal of
1.150 + {outcome = NONE, used_facts, ...} =>
1.151 + (if verbose andalso not auto then
1.152 + let val num_facts = length used_facts in
1.153 + "Found proof with " ^ string_of_int num_facts ^ " fact" ^
1.154 + plural_s num_facts ^ "."
1.155 + |> Output.urgent_message
1.156 + end
1.157 + else
1.158 + ();
1.159 + used_facts |> map fst)
1.160 + | _ => isar_deps
1.161 + end
1.162
1.163
1.164 (*** Low-level communication with MaSh ***)
1.165 @@ -390,9 +457,19 @@
1.166 handle Graph.CYCLES (cycle :: _) =>
1.167 (trace_msg ctxt (fn () =>
1.168 "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
1.169 + | Graph.DUP name =>
1.170 + (trace_msg ctxt (fn () =>
1.171 + "Duplicate fact " ^ quote name ^ " when " ^ when); def)
1.172 | Graph.UNDEF name =>
1.173 (trace_msg ctxt (fn () =>
1.174 "Unknown fact " ^ quote name ^ " when " ^ when); def)
1.175 + | exn =>
1.176 + if Exn.is_interrupt exn then
1.177 + reraise exn
1.178 + else
1.179 + (trace_msg ctxt (fn () =>
1.180 + "Internal error when " ^ when ^ ":\n" ^
1.181 + ML_Compiler.exn_message exn); def)
1.182
1.183 type mash_state = {fact_graph : unit Graph.T}
1.184
1.185 @@ -544,26 +621,41 @@
1.186 (true, "")
1.187 end)
1.188
1.189 +fun sendback sub =
1.190 + Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
1.191 +
1.192 (* Too many dependencies is a sign that a decision procedure is at work. There
1.193 isn't much too learn from such proofs. *)
1.194 val max_dependencies = 10
1.195 -val pass1_learn_timeout_factor = 0.75
1.196 +val commit_timeout = seconds 30.0
1.197
1.198 (* The timeout is understood in a very slack fashion. *)
1.199 -fun mash_learn_facts ctxt ({provers, verbose, overlord, ...} : params) timeout
1.200 - facts =
1.201 +fun mash_learn_facts ctxt (params as {debug, verbose, overlord, timeout, ...})
1.202 + prover auto atp learn_timeout facts =
1.203 let
1.204 val timer = Timer.startRealTimer ()
1.205 - val prover = hd provers
1.206 - fun timed_out frac =
1.207 - Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
1.208 + fun next_commit_time () =
1.209 + Time.+ (Timer.checkRealTimer timer, commit_timeout)
1.210 val {fact_graph} = mash_get ctxt
1.211 val new_facts =
1.212 facts |> filter_out (is_fact_in_graph fact_graph)
1.213 |> sort (thm_ord o pairself snd)
1.214 + val num_new_facts = length new_facts
1.215 in
1.216 + "MaShing" ^
1.217 + (if not auto then
1.218 + " " ^ string_of_int num_new_facts ^ " fact" ^
1.219 + plural_s num_new_facts ^
1.220 + (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "")
1.221 + else
1.222 + "") ^ "..."
1.223 + |> Output.urgent_message;
1.224 if null new_facts then
1.225 - ""
1.226 + if verbose orelse not auto then
1.227 + "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
1.228 + sendback relearn_atpN ^ " to learn from scratch."
1.229 + else
1.230 + ""
1.231 else
1.232 let
1.233 val ths = facts |> map snd
1.234 @@ -571,28 +663,53 @@
1.235 ths |> filter_out is_likely_tautology_or_too_meta
1.236 |> map (rpair () o nickname_of)
1.237 |> Symtab.make
1.238 + fun do_commit [] state = state
1.239 + | do_commit upds {fact_graph} =
1.240 + let
1.241 + val (upds, fact_graph) =
1.242 + ([], fact_graph) |> fold (update_fact_graph ctxt) upds
1.243 + in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end
1.244 fun trim_deps deps = if length deps > max_dependencies then [] else deps
1.245 - fun do_fact _ (accum as (_, true)) = accum
1.246 - | do_fact ((_, stature), th) ((parents, upds), false) =
1.247 + fun commit last upds =
1.248 + (if debug andalso not auto then Output.urgent_message "Committing..."
1.249 + else ();
1.250 + mash_map ctxt (do_commit (rev upds));
1.251 + if not last andalso not auto then
1.252 + let val num_upds = length upds in
1.253 + "Processed " ^ string_of_int num_upds ^ " fact" ^
1.254 + plural_s num_upds ^ " in the last " ^
1.255 + string_from_time commit_timeout ^ "."
1.256 + |> Output.urgent_message
1.257 + end
1.258 + else
1.259 + ())
1.260 + fun do_fact _ (accum as (_, (_, _, _, true))) = accum
1.261 + | do_fact ((_, stature), th)
1.262 + (upds, (parents, n, next_commit, false)) =
1.263 let
1.264 val name = nickname_of th
1.265 val feats =
1.266 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
1.267 - val deps = isabelle_dependencies_of all_names th |> trim_deps
1.268 - val upd = (name, parents, feats, deps)
1.269 - in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
1.270 + val deps =
1.271 + (if atp then atp_dependencies_of ctxt params prover auto facts
1.272 + else isar_dependencies_of) all_names th
1.273 + |> trim_deps
1.274 + val upds = (name, parents, feats, deps) :: upds
1.275 + val (upds, next_commit) =
1.276 + if Time.> (Timer.checkRealTimer timer, next_commit) then
1.277 + (commit false upds; ([], next_commit_time ()))
1.278 + else
1.279 + (upds, next_commit)
1.280 + val timed_out =
1.281 + Time.> (Timer.checkRealTimer timer, learn_timeout)
1.282 + in (upds, ([name], n + 1, next_commit, timed_out)) end
1.283 val parents = parents_wrt_facts facts fact_graph
1.284 - val ((_, upds), _) =
1.285 - ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
1.286 - val n = length upds
1.287 - fun trans {fact_graph} =
1.288 - let
1.289 - val (upds, fact_graph) =
1.290 - ([], fact_graph) |> fold (update_fact_graph ctxt) upds
1.291 - in (mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph}) end
1.292 + val (upds, (_, n, _, _)) =
1.293 + ([], (parents, 0, next_commit_time (), false))
1.294 + |> fold do_fact new_facts
1.295 in
1.296 - mash_map ctxt trans;
1.297 - if verbose then
1.298 + commit true upds;
1.299 + if verbose orelse not auto then
1.300 "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
1.301 (if verbose then
1.302 " in " ^ string_from_time (Timer.checkRealTimer timer)
1.303 @@ -603,15 +720,13 @@
1.304 end
1.305 end
1.306
1.307 -fun mash_learn ctxt params =
1.308 +fun mash_learn ctxt (params as {provers, ...}) atp =
1.309 let
1.310 val thy = Proof_Context.theory_of ctxt
1.311 - val _ = Output.urgent_message "MaShing..."
1.312 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
1.313 val facts = all_facts_of thy css_table
1.314 in
1.315 - mash_learn_facts ctxt params infinite_timeout facts
1.316 - |> (fn "" => "Learned nothing." | msg => msg)
1.317 + mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
1.318 |> Output.urgent_message
1.319 end
1.320
1.321 @@ -634,7 +749,8 @@
1.322 Time.toSeconds timeout >= min_secs_for_learning then
1.323 let val timeout = time_mult learn_timeout_slack timeout in
1.324 launch_thread timeout
1.325 - (fn () => (true, mash_learn_facts ctxt params timeout facts))
1.326 + (fn () => (true, mash_learn_facts ctxt params prover true false
1.327 + timeout facts))
1.328 end
1.329 else
1.330 ()