# HG changeset patch # User blanchet # Date 1479930958 -3600 # Node ID b66f8caf86b6c5aba978f74f21f40920eeae6cfe # Parent 1aef5a0e18d7a970d804fba80fc66585c76b8de1 made MaSh faster and less likely to hang seemingly forever diff -r 1aef5a0e18d7 -r b66f8caf86b6 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Nov 23 16:15:17 2016 +0100 +++ b/src/HOL/TPTP/mash_export.ML Wed Nov 23 20:55:58 2016 +0100 @@ -286,16 +286,16 @@ not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t) -fun generate_mash_suggestions algorithm = +fun generate_mash_suggestions algorithm ctxt = (Options.put_default @{system_option MaSh} algorithm; - Sledgehammer_MaSh.mash_unlearn (); + Sledgehammer_MaSh.mash_unlearn ctxt; generate_mepo_or_mash_suggestions (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts => fn concl_t => tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false Sledgehammer_Util.one_year) #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t - #> fst)) + #> fst) ctxt) fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name = let diff -r 1aef5a0e18d7 -r b66f8caf86b6 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Nov 23 16:15:17 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Nov 23 20:55:58 2016 +0100 @@ -324,10 +324,10 @@ else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then - mash_unlearn () + mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then - (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn () + (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) diff -r 1aef5a0e18d7 -r b66f8caf86b6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Nov 23 16:15:17 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Nov 23 20:55:58 2016 +0100 @@ -69,13 +69,13 @@ val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list - val mash_unlearn : unit -> unit + val mash_unlearn : Proof.context -> unit val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time -> raw_fact list -> string val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit val mash_can_suggest_facts : Proof.context -> bool - val mash_can_suggest_facts_fast : unit -> bool + val mash_can_suggest_facts_fast : Proof.context -> bool val generous_max_suggestions : int -> int val mepo_weight : real @@ -274,6 +274,18 @@ end +(*** Convenience functions for synchronized access ***) + +fun synchronized_timed_value var time_limit = + Synchronized.timed_access var time_limit (fn value => SOME (value, value)) +fun synchronized_timed_change_result var time_limit f = + Synchronized.timed_access var time_limit (SOME o f) +fun synchronized_timed_change var time_limit f = + synchronized_timed_change_result var time_limit (fn x => ((), f x)) + +fun mash_time_limit _ = SOME (seconds 0.1) + + (*** Isabelle-agnostic machine learning ***) structure MaSh = @@ -640,7 +652,7 @@ local -val version = "*** MaSh version 20160805 ***" +val version = "*** MaSh version 20161123 ***" exception FILE_VERSION_TOO_NEW of unit @@ -734,42 +746,49 @@ in fun map_state ctxt f = - Synchronized.change global_state (load_state ctxt ##> f #> save_state ctxt) + (trace_msg ctxt (fn () => "Changing MaSh state"); + synchronized_timed_change global_state mash_time_limit + (load_state ctxt ##> f #> save_state ctxt)) + |> ignore handle FILE_VERSION_TOO_NEW () => () -fun peek_state () = - let val state = Synchronized.value global_state in - if would_load_state state then NONE else SOME state - end +fun peek_state ctxt = + (trace_msg ctxt (fn () => "Peeking at MaSh state"); + (case synchronized_timed_value global_state mash_time_limit of + NONE => NONE + | SOME state => if would_load_state state then NONE else SOME state)) fun get_state ctxt = - Synchronized.change_result global_state (perhaps (try (load_state ctxt)) #> `snd) + (trace_msg ctxt (fn () => "Retrieving MaSh state"); + synchronized_timed_change_result global_state mash_time_limit + (perhaps (try (load_state ctxt)) #> `snd)) -fun clear_state () = - Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state))) +fun clear_state ctxt = + (trace_msg ctxt (fn () => "Clearing MaSh state"); + Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))) end (*** Isabelle helpers ***) -fun crude_printed_term depth t = +fun crude_printed_term size t = let fun term _ (res, 0) = (res, 0) - | term (t $ u) (res, depth) = + | term (t $ u) (res, size) = let - val (res, depth) = term t (res ^ "(", depth) - val (res, depth) = term u (res ^ " ", depth) + val (res, size) = term t (res ^ "(", size) + val (res, size) = term u (res ^ " ", size) in - (res ^ ")", depth) + (res ^ ")", size) end - | term (Abs (s, _, t)) (res, depth) = term t (res ^ "%" ^ s ^ ".", depth - 1) - | term (Bound n) (res, depth) = (res ^ "#" ^ string_of_int n, depth - 1) - | term (Const (s, _)) (res, depth) = (res ^ Long_Name.base_name s, depth - 1) - | term (Free (s, _)) (res, depth) = (res ^ s, depth - 1) - | term (Var ((s, _), _)) (res, depth) = (res ^ s, depth - 1) + | term (Abs (s, _, t)) (res, size) = term t (res ^ "%" ^ s ^ ".", size - 1) + | term (Bound n) (res, size) = (res ^ "#" ^ string_of_int n, size - 1) + | term (Const (s, _)) (res, size) = (res ^ Long_Name.base_name s, size - 1) + | term (Free (s, _)) (res, size) = (res ^ s, size - 1) + | term (Var ((s, _), _)) (res, size) = (res ^ s, size - 1) in - fst (term t ("", depth)) + fst (term t ("", size)) end fun nickname_of_thm th = @@ -778,11 +797,11 @@ (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => - Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 50 (Thm.prop_of th)] + Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 25 (Thm.prop_of th)] | NONE => hint) end else - crude_printed_term 100 (Thm.prop_of th) + crude_printed_term 50 (Thm.prop_of th) fun find_suggested_facts ctxt facts = let @@ -857,23 +876,17 @@ val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] -val pat_tvar_prefix = "_" -val pat_var_prefix = "_" +val crude_str_of_sort = space_implode "," o map Long_Name.base_name o subtract (op =) @{sort type} -(* try "Long_Name.base_name" for shorter names *) -fun massage_long_name s = s - -val crude_str_of_sort = space_implode "," o map massage_long_name o subtract (op =) @{sort type} - -fun crude_str_of_typ (Type (s, [])) = massage_long_name s - | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts) +fun crude_str_of_typ (Type (s, [])) = Long_Name.base_name s + | crude_str_of_typ (Type (s, Ts)) = Long_Name.base_name s ^ implode (map crude_str_of_typ Ts) | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S -fun maybe_singleton_str _ "" = [] - | maybe_singleton_str pref s = [pref ^ s] +fun maybe_singleton_str "" = [] + | maybe_singleton_str s = [s] -val max_pat_breadth = 10 (* FUDGE *) +val max_pat_breadth = 5 (* FUDGE *) fun term_features_of ctxt thy_name term_max_depth type_max_depth ts = let @@ -886,13 +899,12 @@ | add_classes S = fold (`(Sorts.super_classes classes) #> swap #> op :: - #> subtract (op =) @{sort type} #> map massage_long_name + #> subtract (op =) @{sort type} #> map class_feature_of #> union (op =)) S fun pattify_type 0 _ = [] - | pattify_type _ (Type (s, [])) = - if member (op =) bad_types s then [] else [massage_long_name s] + | pattify_type depth (Type (s, [])) = if member (op =) bad_types s then [] else [s] | pattify_type depth (Type (s, U :: Ts)) = let val T = Type (s, Ts) @@ -901,8 +913,8 @@ in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end - | pattify_type _ (TFree (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) - | pattify_type _ (TVar (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) + | pattify_type _ (TFree (_, S)) = maybe_singleton_str (crude_str_of_sort S) + | pattify_type _ (TVar (_, S)) = maybe_singleton_str (crude_str_of_sort S) fun add_type_pat depth T = union (op =) (map type_feature_of (pattify_type depth T)) @@ -918,17 +930,16 @@ | add_subtypes T = add_type T fun pattify_term _ 0 _ = [] - | pattify_term _ _ (Const (s, _)) = - if is_widely_irrelevant_const s then [] else [massage_long_name s] + | pattify_term _ depth (Const (s, _)) = + if is_widely_irrelevant_const s then [] else [s] | pattify_term _ _ (Free (s, T)) = - maybe_singleton_str pat_var_prefix (crude_str_of_typ T) - |> (if member (op =) fixes s then - cons (free_feature_of (massage_long_name (Long_Name.append thy_name s))) - else - I) - | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T) + maybe_singleton_str (crude_str_of_typ T) + |> (if member (op =) fixes s then cons (free_feature_of (Long_Name.append thy_name s)) + else I) + | pattify_term _ _ (Var (_, T)) = + maybe_singleton_str (crude_str_of_typ T) | pattify_term Ts _ (Bound j) = - maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) + maybe_singleton_str (crude_str_of_typ (nth Ts j)) | pattify_term Ts depth (t $ u) = let val ps = take max_pat_breadth (pattify_term Ts depth t) @@ -972,9 +983,9 @@ (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn from such proofs. *) -val max_dependencies = 20 +val max_dependencies = 20 (* FUDGE *) -val prover_default_max_facts = 25 +val prover_default_max_facts = 25 (* FUDGE *) (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) val typedef_dep = nickname_of_thm @{thm CollectI} @@ -1161,7 +1172,7 @@ fun maximal_wrt_access_graph _ [] = [] | maximal_wrt_access_graph access_G (fact :: facts) = let - fun cleanup_wrt (fact as (_, th)) = + fun cleanup_wrt (_, th) = let val thy_id = Thm.theory_id_of_thm th in filter_out (fn (_, th') => Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id)) @@ -1224,54 +1235,57 @@ [Thm.prop_of th] |> features_of ctxt (Thm.theory_name_of_thm th) stature |> map (rpair (weight * factor)) - - val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} = - get_state ctxt + in + (case get_state ctxt of + NONE => ([], []) + | SOME {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} => + let + val goal_feats0 = + features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) + val chained_feats = chained + |> map (rpair 1.0) + |> map (chained_or_extra_features_of chained_feature_factor) + |> rpair [] |-> fold (union (eq_fst (op =))) + val extra_feats = facts + |> take (Int.max (0, num_extra_feature_facts - length chained)) + |> filter fact_has_right_theory + |> weight_facts_steeply + |> map (chained_or_extra_features_of extra_feature_factor) + |> rpair [] |-> fold (union (eq_fst (op =))) - val goal_feats0 = - features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) - val chained_feats = chained - |> map (rpair 1.0) - |> map (chained_or_extra_features_of chained_feature_factor) - |> rpair [] |-> fold (union (eq_fst (op =))) - val extra_feats = facts - |> take (Int.max (0, num_extra_feature_facts - length chained)) - |> filter fact_has_right_theory - |> weight_facts_steeply - |> map (chained_or_extra_features_of extra_feature_factor) - |> rpair [] |-> fold (union (eq_fst (op =))) - - val goal_feats = - fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) - |> debug ? sort (Real.compare o swap o apply2 snd) + val goal_feats = + fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) + |> debug ? sort (Real.compare o swap o apply2 snd) - val parents = maximal_wrt_access_graph access_G facts - val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents) + val parents = maximal_wrt_access_graph access_G facts + val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents) - val suggs = - if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then - let - val learns = - Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G - in - MaSh.query_external ctxt algorithm max_suggs learns goal_feats - end - else - let - val int_goal_feats = - map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats - in - MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs - goal_feats int_goal_feats - end + val suggs = + if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then + let + val learns = + Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) + access_G + in + MaSh.query_external ctxt algorithm max_suggs learns goal_feats + end + else + let + val int_goal_feats = + map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats + in + MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts + max_suggs goal_feats int_goal_feats + end - val unknown = filter_out (is_fact_in_graph access_G o snd) facts - in - find_mash_suggestions ctxt max_suggs suggs facts chained unknown - |> apply2 (map fact_of_raw_fact) + val unknown = filter_out (is_fact_in_graph access_G o snd) facts + in + find_mash_suggestions ctxt max_suggs suggs facts chained unknown + |> apply2 (map fact_of_raw_fact) + end) end -fun mash_unlearn () = (clear_state (); writeln "Reset MaSh") +fun mash_unlearn ctxt = (clear_state ctxt; writeln "Reset MaSh") fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (accum as (access_G, (fact_xtab, feat_xtab))) = @@ -1363,164 +1377,169 @@ let val timer = Timer.startRealTimer () fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout - - val {access_G, ...} = get_state ctxt - val is_in_access_G = is_fact_in_graph access_G o snd - val no_new_facts = forall is_in_access_G facts in - if no_new_facts andalso not run_prover then - if auto_level < 2 then - "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^ - (if auto_level = 0 andalso not run_prover then - "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover" - else - "") - else - "" - else + (case get_state ctxt of + NONE => "MaSh is busy\nPlease try again later" + | SOME {access_G, ...} => let - val name_tabs = build_name_tables nickname_of_thm facts + val is_in_access_G = is_fact_in_graph access_G o snd + val no_new_facts = forall is_in_access_G facts + in + if no_new_facts andalso not run_prover then + if auto_level < 2 then + "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^ + (if auto_level = 0 andalso not run_prover then + "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover" + else + "") + else + "" + else + let + val name_tabs = build_name_tables nickname_of_thm facts - fun deps_of status th = - if status = Non_Rec_Def orelse status = Rec_Def then - SOME [] - else if run_prover then - prover_dependencies_of ctxt params prover auto_level facts name_tabs th - |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) - else - isar_dependencies_of name_tabs th + fun deps_of status th = + if status = Non_Rec_Def orelse status = Rec_Def then + SOME [] + else if run_prover then + prover_dependencies_of ctxt params prover auto_level facts name_tabs th + |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps) + else + isar_dependencies_of name_tabs th - fun do_commit [] [] [] state = state - | do_commit learns relearns flops - {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} = - let - val was_empty = Graph.is_empty access_G + fun do_commit [] [] [] state = state + | do_commit learns relearns flops + {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} = + let + val was_empty = Graph.is_empty access_G - val (learns, (access_G', xtabs')) = - fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs) - |>> map_filter I - val (relearns, access_G'') = - fold_map (relearn_wrt_access_graph ctxt) relearns access_G' + val (learns, (access_G', xtabs')) = + fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs) + |>> map_filter I + val (relearns, access_G'') = + fold_map (relearn_wrt_access_graph ctxt) relearns access_G' - val access_G''' = access_G'' |> fold flop_wrt_access_graph flops - val dirty_facts' = - (case (was_empty, dirty_facts) of - (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names) - | _ => NONE) + val access_G''' = access_G'' |> fold flop_wrt_access_graph flops + val dirty_facts' = + (case (was_empty, dirty_facts) of + (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names) + | _ => NONE) - val (ffds', freqs') = - if null relearns then - recompute_ffds_freqs_from_learns - (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0 - ffds freqs - else - recompute_ffds_freqs_from_access_G access_G''' xtabs' - in - {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs', - dirty_facts = dirty_facts'} - end + val (ffds', freqs') = + if null relearns then + recompute_ffds_freqs_from_learns + (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' + num_facts0 ffds freqs + else + recompute_ffds_freqs_from_access_G access_G''' xtabs' + in + {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs', + dirty_facts = dirty_facts'} + end - fun commit last learns relearns flops = - (if debug andalso auto_level = 0 then writeln "Committing..." else (); - map_state ctxt (do_commit (rev learns) relearns flops); - if not last andalso auto_level = 0 then - let val num_proofs = length learns + length relearns in - writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ - (if run_prover then "automatic" else "Isar") ^ " proof" ^ - plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout) - end - else - ()) + fun commit last learns relearns flops = + (if debug andalso auto_level = 0 then writeln "Committing..." else (); + map_state ctxt (do_commit (rev learns) relearns flops); + if not last andalso auto_level = 0 then + let val num_proofs = length learns + length relearns in + writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ + (if run_prover then "automatic" else "Isar") ^ " proof" ^ + plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout) + end + else + ()) - fun learn_new_fact _ (accum as (_, (_, _, true))) = accum - | learn_new_fact (parents, ((_, stature as (_, status)), th)) - (learns, (num_nontrivial, next_commit, _)) = - let - val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] - val deps = these (deps_of status th) - val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 - val learns = (name, parents, feats, deps) :: learns - val (learns, next_commit) = - if Timer.checkRealTimer timer > next_commit then - (commit false learns [] []; ([], next_commit_time ())) - else - (learns, next_commit) - val timed_out = Timer.checkRealTimer timer > learn_timeout - in - (learns, (num_nontrivial, next_commit, timed_out)) - end + fun learn_new_fact _ (accum as (_, (_, _, true))) = accum + | learn_new_fact (parents, ((_, stature as (_, status)), th)) + (learns, (num_nontrivial, next_commit, _)) = + let + val name = nickname_of_thm th + val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th] + val deps = these (deps_of status th) + val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 + val learns = (name, parents, feats, deps) :: learns + val (learns, next_commit) = + if Timer.checkRealTimer timer > next_commit then + (commit false learns [] []; ([], next_commit_time ())) + else + (learns, next_commit) + val timed_out = Timer.checkRealTimer timer > learn_timeout + in + (learns, (num_nontrivial, next_commit, timed_out)) + end - val (num_new_facts, num_nontrivial) = - if no_new_facts then - (0, 0) - else - let - val new_facts = facts - |> sort (crude_thm_ord ctxt o apply2 snd) - |> attach_parents_to_facts [] - |> filter_out (is_in_access_G o snd) - val (learns, (num_nontrivial, _, _)) = - ([], (0, next_commit_time (), false)) - |> fold learn_new_fact new_facts - in - commit true learns [] []; (length new_facts, num_nontrivial) - end + val (num_new_facts, num_nontrivial) = + if no_new_facts then + (0, 0) + else + let + val new_facts = facts + |> sort (crude_thm_ord ctxt o apply2 snd) + |> attach_parents_to_facts [] + |> filter_out (is_in_access_G o snd) + val (learns, (num_nontrivial, _, _)) = + ([], (0, next_commit_time (), false)) + |> fold learn_new_fact new_facts + in + commit true learns [] []; (length new_facts, num_nontrivial) + end - fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum - | relearn_old_fact ((_, (_, status)), th) - ((relearns, flops), (num_nontrivial, next_commit, _)) = - let - val name = nickname_of_thm th - val (num_nontrivial, relearns, flops) = - (case deps_of status th of - SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops) - | NONE => (num_nontrivial, relearns, name :: flops)) - val (relearns, flops, next_commit) = - if Timer.checkRealTimer timer > next_commit then - (commit false [] relearns flops; ([], [], next_commit_time ())) - else - (relearns, flops, next_commit) - val timed_out = Timer.checkRealTimer timer > learn_timeout - in - ((relearns, flops), (num_nontrivial, next_commit, timed_out)) - end + fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum + | relearn_old_fact ((_, (_, status)), th) + ((relearns, flops), (num_nontrivial, next_commit, _)) = + let + val name = nickname_of_thm th + val (num_nontrivial, relearns, flops) = + (case deps_of status th of + SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops) + | NONE => (num_nontrivial, relearns, name :: flops)) + val (relearns, flops, next_commit) = + if Timer.checkRealTimer timer > next_commit then + (commit false [] relearns flops; ([], [], next_commit_time ())) + else + (relearns, flops, next_commit) + val timed_out = Timer.checkRealTimer timer > learn_timeout + in + ((relearns, flops), (num_nontrivial, next_commit, timed_out)) + end - val num_nontrivial = - if not run_prover then - num_nontrivial - else - let - val max_isar = 1000 * max_dependencies + val num_nontrivial = + if not run_prover then + num_nontrivial + else + let + val max_isar = 1000 * max_dependencies - fun priority_of th = - Random.random_range 0 max_isar + - (case try (Graph.get_node access_G) (nickname_of_thm th) of - SOME (Isar_Proof, _, deps) => ~100 * length deps - | SOME (Automatic_Proof, _, _) => 2 * max_isar - | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar - | NONE => 0) + fun priority_of th = + Random.random_range 0 max_isar + + (case try (Graph.get_node access_G) (nickname_of_thm th) of + SOME (Isar_Proof, _, deps) => ~100 * length deps + | SOME (Automatic_Proof, _, _) => 2 * max_isar + | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar + | NONE => 0) - val old_facts = facts - |> filter is_in_access_G - |> map (`(priority_of o snd)) - |> sort (int_ord o apply2 fst) - |> map snd - val ((relearns, flops), (num_nontrivial, _, _)) = - (([], []), (num_nontrivial, next_commit_time (), false)) - |> fold relearn_old_fact old_facts - in - commit true [] relearns flops; num_nontrivial - end - in - if verbose orelse auto_level < 2 then - "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^ - string_of_int num_nontrivial ^ " nontrivial " ^ - (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^ - (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") - else - "" - end + val old_facts = facts + |> filter is_in_access_G + |> map (`(priority_of o snd)) + |> sort (int_ord o apply2 fst) + |> map snd + val ((relearns, flops), (num_nontrivial, _, _)) = + (([], []), (num_nontrivial, next_commit_time (), false)) + |> fold relearn_old_fact old_facts + in + commit true [] relearns flops; num_nontrivial + end + in + if verbose orelse auto_level < 2 then + "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ + " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^ + (if run_prover then "automatic and " else "") ^ "Isar proof" ^ + plural_s num_nontrivial ^ + (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") + else + "" + end + end) end fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = @@ -1552,21 +1571,23 @@ end fun mash_can_suggest_facts ctxt = - not (Graph.is_empty (#access_G (get_state ctxt))) + (case get_state ctxt of + NONE => false + | SOME {access_G, ...} => not (Graph.is_empty access_G)) -fun mash_can_suggest_facts_fast () = - (case peek_state () of +fun mash_can_suggest_facts_fast ctxt = + (case peek_state ctxt of NONE => false - | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G)); + | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G)) (* Generate more suggestions than requested, because some might be thrown out later for various reasons (e.g., duplicates). *) fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25 -val mepo_weight = 0.5 -val mash_weight = 0.5 +val mepo_weight = 0.5 (* FUDGE *) +val mash_weight = 0.5 (* FUDGE *) -val max_facts_to_learn_before_query = 100 +val max_facts_to_learn_before_query = 100 (* FUDGE *) (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer. *) val min_secs_for_learning = 10 @@ -1600,27 +1621,29 @@ () val mash_enabled = is_mash_enabled () - val mash_fast = mash_can_suggest_facts_fast () + val mash_fast = mash_can_suggest_facts_fast ctxt fun please_learn () = if mash_fast then - let - val {access_G, xtabs = ((num_facts0, _), _), ...} = get_state ctxt - val is_in_access_G = is_fact_in_graph access_G o snd - val min_num_facts_to_learn = length facts - num_facts0 - in - if min_num_facts_to_learn <= max_facts_to_learn_before_query then - (case length (filter_out is_in_access_G facts) of - 0 => () - | num_facts_to_learn => - if num_facts_to_learn <= max_facts_to_learn_before_query then - mash_learn_facts ctxt params prover 2 false timeout facts - |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s)) - else - maybe_launch_thread true num_facts_to_learn) - else - maybe_launch_thread false min_num_facts_to_learn - end + (case get_state ctxt of + NONE => maybe_launch_thread false (length facts) + | SOME {access_G, xtabs = ((num_facts0, _), _), ...} => + let + val is_in_access_G = is_fact_in_graph access_G o snd + val min_num_facts_to_learn = length facts - num_facts0 + in + if min_num_facts_to_learn <= max_facts_to_learn_before_query then + (case length (filter_out is_in_access_G facts) of + 0 => () + | num_facts_to_learn => + if num_facts_to_learn <= max_facts_to_learn_before_query then + mash_learn_facts ctxt params prover 2 false timeout facts + |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s)) + else + maybe_launch_thread true num_facts_to_learn) + else + maybe_launch_thread false min_num_facts_to_learn + end) else maybe_launch_thread false (length facts)