tuning
authorblanchet
Sun Dec 16 19:23:04 2012 +0100 (2012-12-16)
changeset 50570fae8b1d9f701
parent 50569 2019ca8dcbfa
child 50571 b649e33e4821
tuning
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 16 19:13:19 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 16 19:23:04 2012 +0100
     1.3 @@ -370,24 +370,23 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun mash_map ctxt f =
     1.8 +fun map_state ctxt f =
     1.9    Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
    1.10    handle Too_New () => ()
    1.11  
    1.12 -fun mash_peek ctxt f =
    1.13 +fun peek_state ctxt f =
    1.14    Synchronized.change_result global_state
    1.15        (perhaps (try (load ctxt)) #> `snd #>> f)
    1.16  
    1.17 -fun mash_get ctxt =
    1.18 -  Synchronized.change_result global_state (perhaps (try (load ctxt)) #> `snd)
    1.19 -
    1.20 -fun mash_unlearn ctxt =
    1.21 +fun clear_state ctxt =
    1.22    Synchronized.change global_state (fn _ =>
    1.23        (mash_CLEAR ctxt; (* also removes the state file *)
    1.24         (true, empty_state)))
    1.25  
    1.26  end
    1.27  
    1.28 +val mash_unlearn = clear_state
    1.29 +
    1.30  
    1.31  (*** Isabelle helpers ***)
    1.32  
    1.33 @@ -762,7 +761,7 @@
    1.34    let
    1.35      val thy = Proof_Context.theory_of ctxt
    1.36      val (fact_G, suggs) =
    1.37 -      mash_peek ctxt (fn {fact_G, ...} =>
    1.38 +      peek_state ctxt (fn {fact_G, ...} =>
    1.39            if Graph.is_empty fact_G then
    1.40              (fact_G, [])
    1.41            else
    1.42 @@ -825,7 +824,7 @@
    1.43            val feats = features_of ctxt prover thy (Local, General) [t]
    1.44            val deps = used_ths |> map nickname_of
    1.45          in
    1.46 -          mash_peek ctxt (fn {fact_G, ...} =>
    1.47 +          peek_state ctxt (fn {fact_G, ...} =>
    1.48                let val parents = maximal_in_graph fact_G facts in
    1.49                  mash_ADD ctxt overlord [(name, parents, feats, deps)]
    1.50                end);
    1.51 @@ -843,7 +842,7 @@
    1.52      val timer = Timer.startRealTimer ()
    1.53      fun next_commit_time () =
    1.54        Time.+ (Timer.checkRealTimer timer, commit_timeout)
    1.55 -    val {fact_G, ...} = mash_get ctxt
    1.56 +    val {fact_G, ...} = peek_state ctxt I
    1.57      val facts = facts |> sort (thm_ord o pairself snd)
    1.58      val (old_facts, new_facts) =
    1.59        facts |> List.partition (is_fact_in_graph fact_G)
    1.60 @@ -894,7 +893,7 @@
    1.61               Output.urgent_message "Committing..."
    1.62             else
    1.63               ();
    1.64 -           mash_map ctxt (do_commit (rev adds) reps flops);
    1.65 +           map_state ctxt (do_commit (rev adds) reps flops);
    1.66             if not last andalso auto_level = 0 then
    1.67               let val num_proofs = length adds + length reps in
    1.68                 "Learned " ^ string_of_int num_proofs ^ " " ^
    1.69 @@ -1032,7 +1031,8 @@
    1.70    end
    1.71  
    1.72  fun is_mash_enabled () = (getenv "MASH" = "yes")
    1.73 -fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
    1.74 +fun mash_can_suggest_facts ctxt =
    1.75 +  not (Graph.is_empty (#fact_G (peek_state ctxt I)))
    1.76  
    1.77  (* Generate more suggestions than requested, because some might be thrown out
    1.78     later for various reasons. *)