# HG changeset patch # User blanchet # Date 1356700419 -3600 # Node ID b69079c146657882094c5075b460b9a7bceab9f0 # Parent 1ea90e8046dc293fa6c8c640cf0d99d304b4b829 tuned ML function names diff -r 1ea90e8046dc -r b69079c14665 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 10:25:59 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 14:13:39 2012 +0100 @@ -30,11 +30,11 @@ val unescape_metas : string -> string list val encode_features : (string * real) list -> string val extract_query : string -> string * (string * real) list - val mash_CLEAR : Proof.context -> unit - val mash_ADD : + val mash_UNLEARN : Proof.context -> unit + val mash_LEARN : Proof.context -> bool -> (string * string list * (string * real) list * string list) list -> unit - val mash_REPROVE : + val mash_RELEARN : Proof.context -> bool -> (string * string list) list -> unit val mash_QUERY : Proof.context -> bool -> int -> string list * (string * real) list @@ -191,11 +191,11 @@ val encode_features = map encode_feature #> space_implode " " -fun str_of_add (name, parents, feats, deps) = +fun str_of_learn (name, parents, feats, deps) = "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ encode_features feats ^ "; " ^ escape_metas deps ^ "\n" -fun str_of_reprove (name, deps) = +fun str_of_relearn (name, deps) = "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n" fun str_of_query (parents, feats) = @@ -215,26 +215,26 @@ map_filter extract_suggestion (space_explode " " suggs)) | _ => ("", []) -fun mash_CLEAR ctxt = +fun mash_UNLEARN ctxt = let val path = mash_model_dir () in - trace_msg ctxt (K "MaSh CLEAR"); + trace_msg ctxt (K "MaSh UNLEARN"); try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path) NONE; () end -fun mash_ADD _ _ [] = () - | mash_ADD ctxt overlord adds = - (trace_msg ctxt (fn () => "MaSh ADD " ^ - elide_string 1000 (space_implode " " (map #1 adds))); - run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ())) +fun mash_LEARN _ _ [] = () + | mash_LEARN ctxt overlord learns = + (trace_msg ctxt (fn () => "MaSh LEARN " ^ + elide_string 1000 (space_implode " " (map #1 learns))); + run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ())) -fun mash_REPROVE _ _ [] = () - | mash_REPROVE ctxt overlord reps = - (trace_msg ctxt (fn () => "MaSh REPROVE " ^ - elide_string 1000 (space_implode " " (map #1 reps))); - run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ())) +fun mash_RELEARN _ _ [] = () + | mash_RELEARN ctxt overlord relearns = + (trace_msg ctxt (fn () => "MaSh RELEARN " ^ + elide_string 1000 (space_implode " " (map #1 relearns))); + run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = (trace_msg ctxt (fn () => "MaSh QUERY " ^ encode_features feats); @@ -381,7 +381,7 @@ fun clear_state ctxt = Synchronized.change global_state (fn _ => - (mash_CLEAR ctxt; (* also removes the state file *) + (mash_UNLEARN ctxt; (* also removes the state file *) (true, empty_state))) end @@ -784,24 +784,24 @@ val unknown = facts |> filter_out (is_fact_in_graph access_G) in find_mash_suggestions max_facts suggs facts chained unknown end -fun add_wrt_access_graph ctxt (name, parents, feats, deps) (adds, graph) = +fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) = let - fun maybe_add_from from (accum as (parents, graph)) = + fun maybe_learn_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) val graph = graph |> Graph.default_node (name, Isar_Proof) - val (parents, graph) = ([], graph) |> fold maybe_add_from parents - val (deps, _) = ([], graph) |> fold maybe_add_from deps - in ((name, parents, feats, deps) :: adds, graph) end + val (parents, graph) = ([], graph) |> fold maybe_learn_from parents + val (deps, _) = ([], graph) |> fold maybe_learn_from deps + in ((name, parents, feats, deps) :: learns, graph) end -fun reprove_wrt_access_graph ctxt (name, deps) (reps, graph) = +fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = let - fun maybe_rep_from from (accum as (parents, graph)) = + fun maybe_relearn_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) val graph = graph |> update_access_graph_node (name, Automatic_Proof) - val (deps, _) = ([], graph) |> fold maybe_rep_from deps - in ((name, deps) :: reps, graph) end + val (deps, _) = ([], graph) |> fold maybe_relearn_from deps + in ((name, deps) :: relearns, graph) end fun flop_wrt_access_graph name = update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) @@ -834,7 +834,7 @@ in peek_state ctxt (fn {access_G, ...} => let val parents = maximal_in_graph access_G facts in - mash_ADD ctxt overlord [(name, parents, feats, deps)] + mash_LEARN ctxt overlord [(name, parents, feats, deps)] end); (true, "") end) @@ -879,31 +879,31 @@ else isar_dependencies_of all_names th fun do_commit [] [] [] state = state - | do_commit adds reps flops {access_G, dirty} = + | do_commit learns relearns flops {access_G, dirty} = let val was_empty = Graph.is_empty access_G - val (adds, access_G) = - ([], access_G) |> fold (add_wrt_access_graph ctxt) adds - val (reps, access_G) = - ([], access_G) |> fold (reprove_wrt_access_graph ctxt) reps + val (learns, access_G) = + ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns + val (relearns, access_G) = + ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns val access_G = access_G |> fold flop_wrt_access_graph flops val dirty = - case (was_empty, dirty, reps) of - (false, SOME names, []) => SOME (map #1 adds @ names) + case (was_empty, dirty, relearns) of + (false, SOME names, []) => SOME (map #1 learns @ names) | _ => NONE in - mash_ADD ctxt overlord (rev adds); - mash_REPROVE ctxt overlord reps; + mash_LEARN ctxt overlord (rev learns); + mash_RELEARN ctxt overlord relearns; {access_G = access_G, dirty = dirty} end - fun commit last adds reps flops = + fun commit last learns relearns flops = (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else (); - map_state ctxt (do_commit (rev adds) reps flops); + map_state ctxt (do_commit (rev learns) relearns flops); if not last andalso auto_level = 0 then - let val num_proofs = length adds + length reps in + let val num_proofs = length learns + length relearns in "Learned " ^ string_of_int num_proofs ^ " " ^ (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s num_proofs ^ " in the last " ^ @@ -914,24 +914,24 @@ ()) fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum | learn_new_fact ((_, stature as (_, status)), th) - (adds, (parents, n, next_commit, _)) = + (learns, (parents, n, next_commit, _)) = let val name = nickname_of_thm th val feats = features_of ctxt prover (theory_of_thm th) stature [prop_of th] val deps = deps_of status th |> these val n = n |> not (null deps) ? Integer.add 1 - val adds = (name, parents, feats, deps) :: adds - val (adds, next_commit) = + val learns = (name, parents, feats, deps) :: learns + val (learns, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then - (commit false adds [] []; ([], next_commit_time ())) + (commit false learns [] []; ([], next_commit_time ())) else - (adds, next_commit) + (learns, next_commit) val timed_out = case learn_timeout of SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) | NONE => false - in (adds, ([name], n, next_commit, timed_out)) end + in (learns, ([name], n, next_commit, timed_out)) end val n = if null new_facts then 0 @@ -943,29 +943,30 @@ old_facts |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) val parents = maximal_in_graph access_G ancestors - val (adds, (_, n, _, _)) = + val (learns, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) |> fold learn_new_fact new_facts - in commit true adds [] []; n end + in commit true learns [] []; n end fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum | relearn_old_fact ((_, (_, status)), th) - ((reps, flops), (n, next_commit, _)) = + ((relearns, flops), (n, next_commit, _)) = let val name = nickname_of_thm th - val (n, reps, flops) = + val (n, relearns, flops) = case deps_of status th of - SOME deps => (n + 1, (name, deps) :: reps, flops) - | NONE => (n, reps, name :: flops) - val (reps, flops, next_commit) = + SOME deps => (n + 1, (name, deps) :: relearns, flops) + | NONE => (n, relearns, name :: flops) + val (relearns, flops, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then - (commit false [] reps flops; ([], [], next_commit_time ())) + (commit false [] relearns flops; + ([], [], next_commit_time ())) else - (reps, flops, next_commit) + (relearns, flops, next_commit) val timed_out = case learn_timeout of SOME timeout => Time.> (Timer.checkRealTimer timer, timeout) | NONE => false - in ((reps, flops), (n, next_commit, timed_out)) end + in ((relearns, flops), (n, next_commit, timed_out)) end val n = if not run_prover orelse null old_facts then n @@ -988,10 +989,10 @@ old_facts |> map (`priority_of) |> sort (int_ord o pairself fst) |> map snd - val ((reps, flops), (n, _, _)) = + val ((relearns, flops), (n, _, _)) = (([], []), (n, next_commit_time (), false)) |> fold relearn_old_fact old_facts - in commit true [] reps flops; n end + in commit true [] relearns flops; n end in if verbose orelse auto_level < 2 then "Learned " ^ string_of_int n ^ " nontrivial " ^