# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID df75b2d7e26ad14fcbf6c7780c4e0fbd3c804b59 # Parent 641af72b005979d250c45a52b08c42e13f78955e learn command in MaSh diff -r 641af72b0059 -r df75b2d7e26a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200 @@ -35,9 +35,11 @@ val supported_proversN = "supported_provers" val kill_proversN = "kill_provers" val running_proversN = "running_provers" +val unlearnN = "unlearn" +val learnN = "learn" +val relearnN = "relearn" val kill_learnersN = "kill_learners" val running_learnersN = "running_learners" -val unlearnN = "unlearn" val refresh_tptpN = "refresh_tptp" val auto = Unsynchronized.ref false @@ -245,8 +247,7 @@ end)] end -val infinity_time_in_secs = 60 * 60 * 24 * 365 -val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) +val the_timeout = the_default infinite_timeout fun extract_params mode default_params override_params = let @@ -383,12 +384,16 @@ kill_provers () else if subcommand = running_proversN then running_provers () + else if subcommand = unlearnN then + mash_unlearn ctxt + else if subcommand = learnN orelse subcommand = relearnN then + (if subcommand = relearnN then mash_unlearn ctxt else (); + mash_learn ctxt (get_params Normal ctxt + (("verbose", ["true"]) :: override_params))) else if subcommand = kill_learnersN then kill_learners () else if subcommand = running_learnersN then running_learners () - else if subcommand = unlearnN then - mash_unlearn ctxt else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else diff -r 641af72b0059 -r df75b2d7e26a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 @@ -53,10 +53,11 @@ val mash_suggest_facts : Proof.context -> params -> string -> int -> term list -> term -> ('a * thm) list -> ('a * thm) list * ('a * thm) list + val mash_learn_proof : + Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> fact list -> string - val mash_learn_proof : - Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit + val mash_learn : Proof.context -> params -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list @@ -350,12 +351,12 @@ write_file write_access (in_dir ^ "/mash_accessibility"); write_file write_feats (in_dir ^ "/mash_features"); write_file write_deps (in_dir ^ "/mash_dependencies"); - run_mash ctxt overlord info true + run_mash ctxt overlord info false ("--init --inputDir " ^ in_dir ^ and_rm_files overlord " -r" [in_dir]) end -fun run_mash_commands ctxt overlord async save max_suggs write_cmds read_suggs = +fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = let val info as (temp_dir, serial) = mash_info overlord val sugg_file = temp_dir ^ "/mash_suggs" ^ serial @@ -363,7 +364,7 @@ in write_file ([], K "") sugg_file; write_file write_cmds cmd_file; - run_mash ctxt overlord info async + run_mash ctxt overlord info false ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ " --numberOfPredictions " ^ string_of_int max_suggs ^ (if save then " --saveModel" else "") ^ @@ -400,11 +401,11 @@ | mash_ADD ctxt overlord upds = (trace_msg ctxt (fn () => "MaSh ADD " ^ elide_string 1000 (space_implode " " (map #1 upds))); - run_mash_commands ctxt overlord true true 0 (upds, str_of_update) (K ())) + run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ())) fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); - run_mash_commands ctxt overlord false false max_suggs + run_mash_commands ctxt overlord false max_suggs ([query], str_of_query) (fn suggs => snd (extract_query (List.last (suggs ())))) handle List.Empty => []) @@ -548,6 +549,26 @@ val pass1_learn_timeout_factor = 0.5 +fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = + let + val thy = Proof_Context.theory_of ctxt + val prover = hd provers + val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *) + val feats = features_of ctxt prover thy General [t] + val deps = used_ths |> map nickname_of + in + mash_map ctxt (fn {thys, fact_graph} => + let + val parents = parents_wrt_facts facts fact_graph + val upds = [(name, parents, feats, deps)] + val (upds, fact_graph) = + ([], fact_graph) |> fold (update_fact_graph ctxt) upds + in + mash_ADD ctxt overlord upds; + {thys = thys, fact_graph = fact_graph} + end) + end + (* Too many dependencies is a sign that a decision procedure is at work. There isn't much too learn from such proofs. *) val max_dependencies = 10 @@ -596,13 +617,12 @@ ([], fact_graph) |> fold (update_fact_graph ctxt) upds in (mash_INIT_or_ADD ctxt overlord (rev upds); - {thys = thys |> add_thys_for thy, - fact_graph = fact_graph}) + {thys = thys |> add_thys_for thy, fact_graph = fact_graph}) end in mash_map ctxt trans; if verbose then - "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^ + "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^ (if verbose then " in " ^ string_from_time (Timer.checkRealTimer timer) else @@ -612,24 +632,16 @@ end end -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = +fun mash_learn ctxt params = let val thy = Proof_Context.theory_of ctxt - val prover = hd provers - val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *) - val feats = features_of ctxt prover thy General [t] - val deps = used_ths |> map nickname_of + val _ = Output.urgent_message "MaShing..." + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = all_facts_of thy css_table in - mash_map ctxt (fn {thys, fact_graph} => - let - val parents = parents_wrt_facts facts fact_graph - val upds = [(name, parents, feats, deps)] - val (upds, fact_graph) = - ([], fact_graph) |> fold (update_fact_graph ctxt) upds - in - mash_ADD ctxt overlord upds; - {thys = thys, fact_graph = fact_graph} - end) + mash_learn_thy ctxt params thy infinite_timeout facts + |> (fn "" => "Learned nothing." | msg => msg) + |> Output.urgent_message end (* The threshold should be large enough so that MaSh doesn't kick in for Auto diff -r 641af72b0059 -r df75b2d7e26a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 20 22:19:46 2012 +0200 @@ -9,6 +9,7 @@ val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string + val infinite_timeout : Time.time val time_mult : real -> Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option @@ -27,6 +28,8 @@ val serial_commas = Try.serial_commas val simplify_spaces = strip_spaces false (K true) +val infinite_timeout = seconds 31536000.0 (* one year *) + fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))