1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -52,8 +52,8 @@
1.4 val mash_learn_proof :
1.5 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
1.6 -> unit
1.7 - val mash_learn_thy :
1.8 - Proof.context -> params -> theory -> Time.time -> fact list -> string
1.9 + val mash_learn_facts :
1.10 + Proof.context -> params -> Time.time -> fact list -> string
1.11 val mash_learn : Proof.context -> params -> unit
1.12 val relevant_facts :
1.13 Proof.context -> params -> string -> int -> fact_override -> term list
1.14 @@ -394,22 +394,21 @@
1.15 (trace_msg ctxt (fn () =>
1.16 "Unknown fact " ^ quote name ^ " when " ^ when); def)
1.17
1.18 -type mash_state =
1.19 - {thys : bool Symtab.table,
1.20 - fact_graph : unit Graph.T}
1.21 +type mash_state = {fact_graph : unit Graph.T}
1.22
1.23 -val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
1.24 +val empty_state = {fact_graph = Graph.empty}
1.25
1.26 local
1.27
1.28 -fun mash_load _ (state as (true, _)) = state
1.29 - | mash_load ctxt _ =
1.30 +val version = "*** MaSh 0.0 ***"
1.31 +
1.32 +fun load _ (state as (true, _)) = state
1.33 + | load ctxt _ =
1.34 let val path = mash_state_path () in
1.35 (true,
1.36 case try File.read_lines path of
1.37 - SOME (comp_thys :: incomp_thys :: fact_lines) =>
1.38 + SOME (version' :: fact_lines) =>
1.39 let
1.40 - fun add_thy comp thy = Symtab.update (thy, comp)
1.41 fun add_edge_to name parent =
1.42 Graph.default_node (parent, ())
1.43 #> Graph.add_edge (parent, name)
1.44 @@ -419,26 +418,22 @@
1.45 | (name, parents) =>
1.46 Graph.default_node (name, ())
1.47 #> fold (add_edge_to name) parents
1.48 - val thys =
1.49 - Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
1.50 - |> fold (add_thy false) (unescape_metas incomp_thys)
1.51 val fact_graph =
1.52 try_graph ctxt "loading state" Graph.empty (fn () =>
1.53 - Graph.empty |> fold add_fact_line fact_lines)
1.54 - in {thys = thys, fact_graph = fact_graph} end
1.55 + Graph.empty |> version' = version
1.56 + ? fold add_fact_line fact_lines)
1.57 + in {fact_graph = fact_graph} end
1.58 | _ => empty_state)
1.59 end
1.60
1.61 -fun mash_save ({thys, fact_graph, ...} : mash_state) =
1.62 +fun save {fact_graph} =
1.63 let
1.64 val path = mash_state_path ()
1.65 - val thys = Symtab.dest thys
1.66 - val line_for_thys = escape_metas o AList.find (op =) thys
1.67 fun fact_line_for name parents =
1.68 escape_meta name ^ ": " ^ escape_metas parents
1.69 val append_fact = File.append path o suffix "\n" oo fact_line_for
1.70 in
1.71 - File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
1.72 + File.write path (version ^ "\n");
1.73 Graph.fold (fn (name, ((), (parents, _))) => fn () =>
1.74 append_fact name (Graph.Keys.dest parents))
1.75 fact_graph ()
1.76 @@ -450,10 +445,10 @@
1.77 in
1.78
1.79 fun mash_map ctxt f =
1.80 - Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
1.81 + Synchronized.change global_state (load ctxt ##> (f #> tap save))
1.82
1.83 fun mash_get ctxt =
1.84 - Synchronized.change_result global_state (mash_load ctxt #> `snd)
1.85 + Synchronized.change_result global_state (load ctxt #> `snd)
1.86
1.87 fun mash_unlearn ctxt =
1.88 Synchronized.change global_state (fn _ =>
1.89 @@ -504,11 +499,6 @@
1.90 val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
1.91 in (selected, unknown) end
1.92
1.93 -fun add_thys_for thy =
1.94 - let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
1.95 - add false thy #> fold (add true) (Theory.ancestors_of thy)
1.96 - end
1.97 -
1.98 fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
1.99 let
1.100 fun maybe_add_from from (accum as (parents, graph)) =
1.101 @@ -542,15 +532,14 @@
1.102 val feats = features_of ctxt prover thy (Local, General) [t]
1.103 val deps = used_ths |> map nickname_of
1.104 in
1.105 - mash_map ctxt (fn {thys, fact_graph} =>
1.106 + mash_map ctxt (fn {fact_graph} =>
1.107 let
1.108 val parents = parents_wrt_facts facts fact_graph
1.109 val upds = [(name, parents, feats, deps)]
1.110 val (upds, fact_graph) =
1.111 ([], fact_graph) |> fold (update_fact_graph ctxt) upds
1.112 in
1.113 - mash_ADD ctxt overlord upds;
1.114 - {thys = thys, fact_graph = fact_graph}
1.115 + mash_ADD ctxt overlord upds; {fact_graph = fact_graph}
1.116 end);
1.117 (true, "")
1.118 end)
1.119 @@ -561,14 +550,14 @@
1.120 val pass1_learn_timeout_factor = 0.75
1.121
1.122 (* The timeout is understood in a very slack fashion. *)
1.123 -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
1.124 - facts =
1.125 +fun mash_learn_facts ctxt ({provers, verbose, overlord, ...} : params) timeout
1.126 + facts =
1.127 let
1.128 val timer = Timer.startRealTimer ()
1.129 val prover = hd provers
1.130 fun timed_out frac =
1.131 Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
1.132 - val {fact_graph, ...} = mash_get ctxt
1.133 + val {fact_graph} = mash_get ctxt
1.134 val new_facts =
1.135 facts |> filter_out (is_fact_in_graph fact_graph)
1.136 |> sort (thm_ord o pairself snd)
1.137 @@ -596,14 +585,11 @@
1.138 val ((_, upds), _) =
1.139 ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
1.140 val n = length upds
1.141 - fun trans {thys, fact_graph} =
1.142 + fun trans {fact_graph} =
1.143 let
1.144 val (upds, fact_graph) =
1.145 ([], fact_graph) |> fold (update_fact_graph ctxt) upds
1.146 - in
1.147 - (mash_ADD ctxt overlord (rev upds);
1.148 - {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
1.149 - end
1.150 + in (mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph}) end
1.151 in
1.152 mash_map ctxt trans;
1.153 if verbose then
1.154 @@ -624,7 +610,7 @@
1.155 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
1.156 val facts = all_facts_of thy css_table
1.157 in
1.158 - mash_learn_thy ctxt params thy infinite_timeout facts
1.159 + mash_learn_facts ctxt params infinite_timeout facts
1.160 |> (fn "" => "Learned nothing." | msg => msg)
1.161 |> Output.urgent_message
1.162 end
1.163 @@ -643,13 +629,12 @@
1.164 []
1.165 else
1.166 let
1.167 - val thy = Proof_Context.theory_of ctxt
1.168 fun maybe_learn () =
1.169 if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
1.170 Time.toSeconds timeout >= min_secs_for_learning then
1.171 let val timeout = time_mult learn_timeout_slack timeout in
1.172 launch_thread timeout
1.173 - (fn () => (true, mash_learn_thy ctxt params thy timeout facts))
1.174 + (fn () => (true, mash_learn_facts ctxt params timeout facts))
1.175 end
1.176 else
1.177 ()