1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -35,9 +35,11 @@
     1.4  val supported_proversN = "supported_provers"
     1.5  val kill_proversN = "kill_provers"
     1.6  val running_proversN = "running_provers"
     1.7 +val unlearnN = "unlearn"
     1.8 +val learnN = "learn"
     1.9 +val relearnN = "relearn"
    1.10  val kill_learnersN = "kill_learners"
    1.11  val running_learnersN = "running_learners"
    1.12 -val unlearnN = "unlearn"
    1.13  val refresh_tptpN = "refresh_tptp"
    1.14  
    1.15  val auto = Unsynchronized.ref false
    1.16 @@ -245,8 +247,7 @@
    1.17                           end)]
    1.18    end
    1.19  
    1.20 -val infinity_time_in_secs = 60 * 60 * 24 * 365
    1.21 -val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
    1.22 +val the_timeout = the_default infinite_timeout
    1.23  
    1.24  fun extract_params mode default_params override_params =
    1.25    let
    1.26 @@ -383,12 +384,16 @@
    1.27        kill_provers ()
    1.28      else if subcommand = running_proversN then
    1.29        running_provers ()
    1.30 +    else if subcommand = unlearnN then
    1.31 +      mash_unlearn ctxt
    1.32 +    else if subcommand = learnN orelse subcommand = relearnN then
    1.33 +      (if subcommand = relearnN then mash_unlearn ctxt else ();
    1.34 +       mash_learn ctxt (get_params Normal ctxt
    1.35 +                                   (("verbose", ["true"]) :: override_params)))
    1.36      else if subcommand = kill_learnersN then
    1.37        kill_learners ()
    1.38      else if subcommand = running_learnersN then
    1.39        running_learners ()
    1.40 -    else if subcommand = unlearnN then
    1.41 -      mash_unlearn ctxt
    1.42      else if subcommand = refresh_tptpN then
    1.43        refresh_systems_on_tptp ()
    1.44      else

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     2.3 @@ -53,10 +53,11 @@
     2.4    val mash_suggest_facts :
     2.5      Proof.context -> params -> string -> int -> term list -> term
     2.6      -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
     2.7 +  val mash_learn_proof :
     2.8 +    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
     2.9    val mash_learn_thy :
    2.10      Proof.context -> params -> theory -> Time.time -> fact list -> string
    2.11 -  val mash_learn_proof :
    2.12 -    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
    2.13 +  val mash_learn : Proof.context -> params -> unit
    2.14    val relevant_facts :
    2.15      Proof.context -> params -> string -> int -> fact_override -> term list
    2.16      -> term -> fact list -> fact list
    2.17 @@ -350,12 +351,12 @@
    2.18      write_file write_access (in_dir ^ "/mash_accessibility");
    2.19      write_file write_feats (in_dir ^ "/mash_features");
    2.20      write_file write_deps (in_dir ^ "/mash_dependencies");
    2.21 -    run_mash ctxt overlord info true
    2.22 +    run_mash ctxt overlord info false
    2.23               ("--init --inputDir " ^ in_dir ^
    2.24                and_rm_files overlord " -r" [in_dir])
    2.25    end
    2.26  
    2.27 -fun run_mash_commands ctxt overlord async save max_suggs write_cmds read_suggs =
    2.28 +fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
    2.29    let
    2.30      val info as (temp_dir, serial) = mash_info overlord
    2.31      val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
    2.32 @@ -363,7 +364,7 @@
    2.33    in
    2.34      write_file ([], K "") sugg_file;
    2.35      write_file write_cmds cmd_file;
    2.36 -    run_mash ctxt overlord info async
    2.37 +    run_mash ctxt overlord info false
    2.38               ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
    2.39                " --numberOfPredictions " ^ string_of_int max_suggs ^
    2.40                (if save then " --saveModel" else "") ^
    2.41 @@ -400,11 +401,11 @@
    2.42    | mash_ADD ctxt overlord upds =
    2.43      (trace_msg ctxt (fn () => "MaSh ADD " ^
    2.44           elide_string 1000 (space_implode " " (map #1 upds)));
    2.45 -     run_mash_commands ctxt overlord true true 0 (upds, str_of_update) (K ()))
    2.46 +     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
    2.47  
    2.48  fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
    2.49    (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
    2.50 -   run_mash_commands ctxt overlord false false max_suggs
    2.51 +   run_mash_commands ctxt overlord false  max_suggs
    2.52         ([query], str_of_query)
    2.53         (fn suggs => snd (extract_query (List.last (suggs ()))))
    2.54     handle List.Empty => [])
    2.55 @@ -548,6 +549,26 @@
    2.56  
    2.57  val pass1_learn_timeout_factor = 0.5
    2.58  
    2.59 +fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
    2.60 +  let
    2.61 +    val thy = Proof_Context.theory_of ctxt
    2.62 +    val prover = hd provers
    2.63 +    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
    2.64 +    val feats = features_of ctxt prover thy General [t]
    2.65 +    val deps = used_ths |> map nickname_of
    2.66 +  in
    2.67 +    mash_map ctxt (fn {thys, fact_graph} =>
    2.68 +        let
    2.69 +          val parents = parents_wrt_facts facts fact_graph
    2.70 +          val upds = [(name, parents, feats, deps)]
    2.71 +          val (upds, fact_graph) =
    2.72 +            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    2.73 +        in
    2.74 +          mash_ADD ctxt overlord upds;
    2.75 +          {thys = thys, fact_graph = fact_graph}
    2.76 +        end)
    2.77 +  end
    2.78 +
    2.79  (* Too many dependencies is a sign that a decision procedure is at work. There
    2.80     isn't much too learn from such proofs. *)
    2.81  val max_dependencies = 10
    2.82 @@ -596,13 +617,12 @@
    2.83                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
    2.84            in
    2.85              (mash_INIT_or_ADD ctxt overlord (rev upds);
    2.86 -             {thys = thys |> add_thys_for thy,
    2.87 -              fact_graph = fact_graph})
    2.88 +             {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
    2.89            end
    2.90        in
    2.91          mash_map ctxt trans;
    2.92          if verbose then
    2.93 -          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
    2.94 +          "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
    2.95            (if verbose then
    2.96               " in " ^ string_from_time (Timer.checkRealTimer timer)
    2.97             else
    2.98 @@ -612,24 +632,16 @@
    2.99        end
   2.100    end
   2.101  
   2.102 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
   2.103 +fun mash_learn ctxt params =
   2.104    let
   2.105      val thy = Proof_Context.theory_of ctxt
   2.106 -    val prover = hd provers
   2.107 -    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
   2.108 -    val feats = features_of ctxt prover thy General [t]
   2.109 -    val deps = used_ths |> map nickname_of
   2.110 +    val _ = Output.urgent_message "MaShing..."
   2.111 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
   2.112 +    val facts = all_facts_of thy css_table
   2.113    in
   2.114 -    mash_map ctxt (fn {thys, fact_graph} =>
   2.115 -        let
   2.116 -          val parents = parents_wrt_facts facts fact_graph
   2.117 -          val upds = [(name, parents, feats, deps)]
   2.118 -          val (upds, fact_graph) =
   2.119 -            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   2.120 -        in
   2.121 -          mash_ADD ctxt overlord upds;
   2.122 -          {thys = thys, fact_graph = fact_graph}
   2.123 -        end)
   2.124 +     mash_learn_thy ctxt params thy infinite_timeout facts
   2.125 +     |> (fn "" => "Learned nothing." | msg => msg)
   2.126 +     |> Output.urgent_message
   2.127    end
   2.128  
   2.129  (* The threshold should be large enough so that MaSh doesn't kick in for Auto

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:46 2012 +0200
     3.3 @@ -9,6 +9,7 @@
     3.4    val plural_s : int -> string
     3.5    val serial_commas : string -> string list -> string list
     3.6    val simplify_spaces : string -> string
     3.7 +  val infinite_timeout : Time.time
     3.8    val time_mult : real -> Time.time -> Time.time
     3.9    val parse_bool_option : bool -> string -> string -> bool option
    3.10    val parse_time_option : string -> string -> Time.time option
    3.11 @@ -27,6 +28,8 @@
    3.12  val serial_commas = Try.serial_commas
    3.13  val simplify_spaces = strip_spaces false (K true)
    3.14  
    3.15 +val infinite_timeout = seconds 31536000.0 (* one year *)
    3.16 +
    3.17  fun time_mult k t =
    3.18    Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
    3.19