1.1 --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
1.3 @@ -134,7 +134,7 @@
1.4 atp_problem
1.5 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
1.6 val ths = facts |> map snd
1.7 - val all_names = ths |> map Thm.get_name_hint
1.8 + val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make
1.9 val infers =
1.10 facts |> map (fn (_, th) =>
1.11 (fact_name_of (Thm.get_name_hint th),
2.1 --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
2.2 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
2.3 @@ -26,6 +26,10 @@
2.4
2.5 val max_facts_slack = 2
2.6
2.7 +val all_names =
2.8 + filter_out (is_likely_tautology orf is_too_meta)
2.9 + #> map (rpair () o Thm.get_name_hint) #> Symtab.make
2.10 +
2.11 fun evaluate_mash_suggestions ctxt params thy file_name =
2.12 let
2.13 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
2.14 @@ -36,10 +40,7 @@
2.15 val lines = path |> File.read_lines
2.16 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.17 val facts = all_facts_of thy css_table
2.18 - val all_names =
2.19 - facts |> map snd
2.20 - |> filter_out (is_likely_tautology orf is_too_meta)
2.21 - |> map Thm.get_name_hint
2.22 + val all_names = all_names (facts |> map snd)
2.23 val iter_ok = Unsynchronized.ref 0
2.24 val mash_ok = Unsynchronized.ref 0
2.25 val mesh_ok = Unsynchronized.ref 0
3.1 --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
3.2 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
3.3 @@ -26,8 +26,31 @@
3.4 open Sledgehammer_Filter_Iter
3.5 open Sledgehammer_Filter_MaSh
3.6
3.7 +fun thy_map_from_facts ths =
3.8 + ths |> sort (thm_ord o swap o pairself snd)
3.9 + |> map (snd #> `(theory_of_thm #> Context.theory_name))
3.10 + |> AList.coalesce (op =)
3.11 + |> map (apsnd (map Thm.get_name_hint))
3.12 +
3.13 +fun has_thy thy th =
3.14 + Context.theory_name thy = Context.theory_name (theory_of_thm th)
3.15 +
3.16 +fun parent_facts thy thy_map =
3.17 + let
3.18 + fun add_last thy =
3.19 + case AList.lookup (op =) thy_map (Context.theory_name thy) of
3.20 + SOME (last_fact :: _) => insert (op =) last_fact
3.21 + | _ => add_parent thy
3.22 + and add_parent thy = fold add_last (Theory.parents_of thy)
3.23 + in add_parent thy [] end
3.24 +
3.25 +val thy_name_of_fact = hd o Long_Name.explode
3.26 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
3.27
3.28 +val all_names =
3.29 + filter_out (is_likely_tautology orf is_too_meta)
3.30 + #> map (rpair () o Thm.get_name_hint) #> Symtab.make
3.31 +
3.32 fun generate_accessibility thy include_thy file_name =
3.33 let
3.34 val path = file_name |> Path.explode
3.35 @@ -72,9 +95,7 @@
3.36 all_facts_of thy Termtab.empty
3.37 |> not include_thy ? filter_out (has_thy thy o snd)
3.38 |> map snd
3.39 - val all_names =
3.40 - ths |> filter_out (is_likely_tautology orf is_too_meta)
3.41 - |> map Thm.get_name_hint
3.42 + val all_names = all_names ths
3.43 fun do_thm th =
3.44 let
3.45 val name = Thm.get_name_hint th
3.46 @@ -92,9 +113,7 @@
3.47 all_facts_of thy Termtab.empty
3.48 |> not include_thy ? filter_out (has_thy thy o snd)
3.49 val ths = facts |> map snd
3.50 - val all_names =
3.51 - ths |> filter_out (is_likely_tautology orf is_too_meta)
3.52 - |> map Thm.get_name_hint
3.53 + val all_names = all_names ths
3.54 fun is_dep dep (_, th) = Thm.get_name_hint th = dep
3.55 fun add_isa_dep facts dep accum =
3.56 if exists (is_dep dep) accum then
3.57 @@ -142,9 +161,7 @@
3.58 facts |> List.partition (has_thy thy o snd)
3.59 |>> sort (thm_ord o pairself snd)
3.60 val ths = facts |> map snd
3.61 - val all_names =
3.62 - ths |> filter_out (is_likely_tautology orf is_too_meta)
3.63 - |> map Thm.get_name_hint
3.64 + val all_names = all_names ths
3.65 fun do_fact ((_, (_, status)), th) prevs =
3.66 let
3.67 val name = Thm.get_name_hint th
4.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200
4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200
4.3 @@ -91,12 +91,6 @@
4.4 InternalError |
4.5 UnknownError of string
4.6
4.7 -fun elide_string threshold s =
4.8 - if size s > threshold then
4.9 - String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
4.10 - String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
4.11 - else
4.12 - s
4.13 fun short_output verbose output =
4.14 if verbose then
4.15 if output = "" then "No details available" else elide_string 1000 output
5.1 --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 18 08:44:04 2012 +0200
5.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 18 08:44:04 2012 +0200
5.3 @@ -12,6 +12,7 @@
5.4 val stringN_of_int : int -> int -> string
5.5 val strip_spaces : bool -> (char -> bool) -> string -> string
5.6 val strip_spaces_except_between_idents : string -> string
5.7 + val elide_string : int -> string -> string
5.8 val nat_subscript : int -> string
5.9 val unyxml : string -> string
5.10 val maybe_quote : string -> string
5.11 @@ -106,6 +107,13 @@
5.12 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
5.13 val strip_spaces_except_between_idents = strip_spaces true is_ident_char
5.14
5.15 +fun elide_string threshold s =
5.16 + if size s > threshold then
5.17 + String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
5.18 + String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
5.19 + else
5.20 + s
5.21 +
5.22 val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
5.23 fun nat_subscript n =
5.24 n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
6.3 @@ -30,27 +30,27 @@
6.4 val is_too_meta : thm -> bool
6.5 val theory_ord : theory * theory -> order
6.6 val thm_ord : thm * thm -> order
6.7 - val thy_map_from_facts : fact list -> (string * string list) list
6.8 - val has_thy : theory -> thm -> bool
6.9 - val parent_facts : theory -> (string * string list) list -> string list
6.10 val features_of : theory -> status -> term list -> string list
6.11 - val isabelle_dependencies_of : string list -> thm -> string list
6.12 + val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
6.13 val goal_of_thm : theory -> thm -> thm
6.14 val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
6.15 - val thy_name_of_fact : string -> string
6.16 val mash_RESET : Proof.context -> unit
6.17 + val mash_INIT :
6.18 + Proof.context -> bool
6.19 + -> (string * string list * string list * string list) list -> unit
6.20 val mash_ADD :
6.21 - Proof.context -> (string * string list * string list * string list) list
6.22 - -> unit
6.23 - val mash_DEL : Proof.context -> string list -> string list -> unit
6.24 - val mash_QUERY : Proof.context -> string list * string list -> string list
6.25 + Proof.context -> bool
6.26 + -> (string * string list * string list * string list) list -> unit
6.27 + val mash_QUERY :
6.28 + Proof.context -> bool -> string list * string list -> string list
6.29 val mash_reset : Proof.context -> unit
6.30 val mash_can_suggest_facts : Proof.context -> bool
6.31 val mash_suggest_facts :
6.32 Proof.context -> params -> string -> term list -> term -> fact list
6.33 -> fact list
6.34 - val mash_learn_thy : Proof.context -> theory -> real -> unit
6.35 - val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit
6.36 + val mash_learn_thy : Proof.context -> params -> theory -> real -> unit
6.37 + val mash_learn_proof :
6.38 + Proof.context -> params -> term -> thm list -> fact list -> unit
6.39 val relevant_facts :
6.40 Proof.context -> params -> string -> int -> fact_override -> term list
6.41 -> term -> fact list -> fact list
6.42 @@ -79,7 +79,7 @@
6.43 fun mash_home () = getenv "MASH_HOME"
6.44 fun mash_state_dir () =
6.45 getenv "ISABELLE_HOME_USER" ^ "/mash"
6.46 - |> tap (fn dir => Isabelle_System.mkdir (Path.explode dir))
6.47 + |> tap (Isabelle_System.mkdir o Path.explode)
6.48 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
6.49
6.50 (*** Isabelle helpers ***)
6.51 @@ -161,10 +161,11 @@
6.52 exists_Const (fn (c, T) =>
6.53 not (is_conn c) andalso exists has_bool (binder_types T))
6.54
6.55 -fun higher_inst_const thy (c, T) =
6.56 +fun higher_inst_const thy (s, T) =
6.57 case binder_types T of
6.58 [] => false
6.59 - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
6.60 + | Ts => length (binder_types (Sign.the_const_type thy s)) <> length Ts
6.61 + handle TYPE _ => false
6.62
6.63 val binders = [@{const_name All}, @{const_name Ex}]
6.64
6.65 @@ -246,24 +247,6 @@
6.66
6.67 val thm_ord = theory_ord o pairself theory_of_thm
6.68
6.69 -fun thy_map_from_facts ths =
6.70 - ths |> sort (thm_ord o swap o pairself snd)
6.71 - |> map (snd #> `(theory_of_thm #> Context.theory_name))
6.72 - |> AList.coalesce (op =)
6.73 - |> map (apsnd (map Thm.get_name_hint))
6.74 -
6.75 -fun has_thy thy th =
6.76 - Context.theory_name thy = Context.theory_name (theory_of_thm th)
6.77 -
6.78 -fun parent_facts thy thy_map =
6.79 - let
6.80 - fun add_last thy =
6.81 - case AList.lookup (op =) thy_map (Context.theory_name thy) of
6.82 - SOME (last_fact :: _) => insert (op =) last_fact
6.83 - | _ => add_parent thy
6.84 - and add_parent thy = fold add_last (Theory.parents_of thy)
6.85 - in add_parent thy [] end
6.86 -
6.87 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
6.88
6.89 val term_max_depth = 1
6.90 @@ -310,41 +293,67 @@
6.91 Sledgehammer_Provers.Normal (hd provers)
6.92 in prover params (K (K (K ""))) problem end
6.93
6.94 -fun accessibility_of thy thy_map =
6.95 - case AList.lookup (op =) thy_map (Context.theory_name thy) of
6.96 - SOME (fact :: _) => [fact]
6.97 - | _ => parent_facts thy thy_map
6.98 -
6.99 -val thy_name_of_fact = hd o Long_Name.explode
6.100 -
6.101
6.102 (*** Low-level communication with MaSh ***)
6.103
6.104 -fun run_mash ctxt save write_cmds read_preds =
6.105 +val max_preds = 500
6.106 +
6.107 +fun mash_info overlord =
6.108 + if overlord then (getenv "ISABELLE_HOME_USER", "")
6.109 + else (getenv "ISABELLE_TMP", serial_string ())
6.110 +
6.111 +fun run_mash ctxt (temp_dir, serial) core =
6.112 let
6.113 - val temp_dir = getenv "ISABELLE_TMP"
6.114 - val serial = serial_string ()
6.115 - val cmd_file = temp_dir ^ "/mash_commands." ^ serial
6.116 - val cmd_path = Path.explode cmd_file
6.117 - val pred_file = temp_dir ^ "/mash_preds." ^ serial
6.118 - val log_file = temp_dir ^ "/mash_log." ^ serial
6.119 + val log_file = temp_dir ^ "/mash_log" ^ serial
6.120 + val err_file = temp_dir ^ "/mash_err" ^ serial
6.121 val command =
6.122 - mash_home () ^ "/mash.py --quiet --inputFile " ^ cmd_file ^
6.123 - " --outputDir " ^ mash_state_dir () ^ " --predictions " ^ pred_file ^
6.124 - " --log " ^ log_file ^ " --numberOfPredictions 1000" ^
6.125 - (if save then " --saveModel" else "")
6.126 - val _ = File.write cmd_path ""
6.127 - val _ = write_cmds (File.append cmd_path)
6.128 - val _ = trace_msg ctxt (fn () => " running " ^ command)
6.129 - val _ = Isabelle_System.bash command
6.130 - in read_preds (fn () => File.read_lines (Path.explode pred_file)) end
6.131 + mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
6.132 + " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
6.133 + in
6.134 + trace_msg ctxt (fn () => "Running " ^ command);
6.135 + Isabelle_System.bash command; ()
6.136 + end
6.137
6.138 -fun str_of_update (fact, access, feats, deps) =
6.139 - "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^
6.140 +fun write_file write file =
6.141 + let val path = Path.explode file in
6.142 + File.write path ""; write (File.append path)
6.143 + end
6.144 +
6.145 +fun run_mash_init ctxt overlord write_access write_feats write_deps =
6.146 + let
6.147 + val info as (temp_dir, serial) = mash_info overlord
6.148 + val in_dir = temp_dir ^ "/mash_init" ^ serial
6.149 + |> tap (Isabelle_System.mkdir o Path.explode)
6.150 + in
6.151 + write_file write_access (in_dir ^ "/mash_accessibility");
6.152 + write_file write_feats (in_dir ^ "/mash_features");
6.153 + write_file write_deps (in_dir ^ "/mash_dependencies");
6.154 + run_mash ctxt info ("--init --inputDir " ^ in_dir)
6.155 + end
6.156 +
6.157 +fun run_mash_commands ctxt overlord save write_cmds read_preds =
6.158 + let
6.159 + val info as (temp_dir, serial) = mash_info overlord
6.160 + val cmd_file = temp_dir ^ "/mash_commands" ^ serial
6.161 + val pred_file = temp_dir ^ "/mash_preds" ^ serial
6.162 + in
6.163 + write_file write_cmds cmd_file;
6.164 + run_mash ctxt info
6.165 + ("--inputFile " ^ cmd_file ^ " --predictions " ^ pred_file ^
6.166 + " --numberOfPredictions " ^ string_of_int max_preds ^
6.167 + (if save then " --saveModel" else ""));
6.168 + read_preds (fn () => File.read_lines (Path.explode pred_file))
6.169 + end
6.170 +
6.171 +fun str_of_update (name, parents, feats, deps) =
6.172 + "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
6.173 escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
6.174
6.175 -fun str_of_query (access, feats) =
6.176 - "? " ^ escape_metas access ^ "; " ^ escape_metas feats
6.177 +fun str_of_query (parents, feats) =
6.178 + "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
6.179 +
6.180 +fun init_str_of_update get (upd as (name, _, _, _)) =
6.181 + escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
6.182
6.183 fun mash_RESET ctxt =
6.184 let val path = mash_state_dir () |> Path.explode in
6.185 @@ -354,30 +363,37 @@
6.186 path ()
6.187 end
6.188
6.189 -fun mash_ADD _ [] = ()
6.190 - | mash_ADD ctxt upds =
6.191 - (trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds));
6.192 - run_mash ctxt true (fn append => List.app (append o str_of_update) upds)
6.193 - (K ()))
6.194 +fun mash_INIT ctxt _ [] = mash_RESET ctxt
6.195 + | mash_INIT ctxt overlord upds =
6.196 + (trace_msg ctxt (fn () => "MaSh INIT " ^
6.197 + elide_string 1000 (space_implode " " (map #1 upds)));
6.198 + run_mash_init ctxt overlord
6.199 + (fn append => List.app (append o init_str_of_update #2) upds)
6.200 + (fn append => List.app (append o init_str_of_update #3) upds)
6.201 + (fn append => List.app (append o init_str_of_update #4) upds))
6.202
6.203 -fun mash_DEL ctxt facts feats =
6.204 - trace_msg ctxt (fn () =>
6.205 - "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats)
6.206 +fun mash_ADD _ _ [] = ()
6.207 + | mash_ADD ctxt overlord upds =
6.208 + (trace_msg ctxt (fn () => "MaSh ADD " ^
6.209 + elide_string 1000 (space_implode " " (map #1 upds)));
6.210 + run_mash_commands ctxt overlord true
6.211 + (fn append => List.app (append o str_of_update) upds) (K ()))
6.212
6.213 -fun mash_QUERY ctxt (query as (_, feats)) =
6.214 +fun mash_QUERY ctxt overlord (query as (_, feats)) =
6.215 (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
6.216 - run_mash ctxt false (fn append => append (str_of_query query))
6.217 - (fn preds => snd (extract_query (List.last (preds ()))))
6.218 + run_mash_commands ctxt overlord false
6.219 + (fn append => append (str_of_query query))
6.220 + (fn preds => snd (extract_query (List.last (preds ()))))
6.221 handle List.Empty => [])
6.222
6.223
6.224 (*** High-level communication with MaSh ***)
6.225
6.226 type mash_state =
6.227 - {dirty_thys : string list,
6.228 - thy_map : (string * string list) list}
6.229 + {thys : bool Symtab.table,
6.230 + fact_graph : unit Graph.T}
6.231
6.232 -val empty_state = {dirty_thys = [], thy_map = []}
6.233 +val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
6.234
6.235 local
6.236
6.237 @@ -386,27 +402,35 @@
6.238 let val path = mash_state_path () in
6.239 (true,
6.240 case try File.read_lines path of
6.241 - SOME (dirty_line :: facts_lines) =>
6.242 + SOME (comp_thys :: incomp_thys :: fact_lines) =>
6.243 let
6.244 - fun add_facts_line line =
6.245 - case unescape_metas line of
6.246 - thy :: facts => cons (thy, facts)
6.247 - | _ => I (* shouldn't happen *)
6.248 - in
6.249 - {dirty_thys = unescape_metas dirty_line,
6.250 - thy_map = fold_rev add_facts_line facts_lines []}
6.251 - end
6.252 + fun add_thy comp thy = Symtab.update (thy, comp)
6.253 + fun add_fact_line line =
6.254 + case extract_query line of
6.255 + ("", _) => I (* shouldn't happen *)
6.256 + | (name, parents) =>
6.257 + Graph.default_node (name, ())
6.258 + #> fold (fn par => Graph.add_edge (par, name)) parents
6.259 + val thys =
6.260 + Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
6.261 + |> fold (add_thy false) (unescape_metas incomp_thys)
6.262 + val fact_graph = Graph.empty |> fold add_fact_line fact_lines
6.263 + in {thys = thys, fact_graph = fact_graph} end
6.264 | _ => empty_state)
6.265 end
6.266
6.267 -fun mash_save ({dirty_thys, thy_map} : mash_state) =
6.268 +fun mash_save ({thys, fact_graph, ...} : mash_state) =
6.269 let
6.270 val path = mash_state_path ()
6.271 - val dirty_line = escape_metas dirty_thys ^ "\n"
6.272 - fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n"
6.273 + val thys = Symtab.dest thys
6.274 + fun line_for_thys comp = AList.find (op =) thys comp |> escape_metas
6.275 + fun fact_line_for name parents = name :: parents |> escape_metas
6.276 + val append_fact = File.append path o suffix "\n" oo fact_line_for
6.277 in
6.278 - File.write path dirty_line;
6.279 - List.app (File.append path o fact_line_for) thy_map
6.280 + File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
6.281 + Graph.fold (fn (name, ((), (parents, _))) => fn () =>
6.282 + append_fact name (Graph.Keys.dest parents))
6.283 + fact_graph ()
6.284 end
6.285
6.286 val global_state =
6.287 @@ -427,52 +451,51 @@
6.288 end
6.289
6.290 fun mash_can_suggest_facts (_ : Proof.context) =
6.291 - mash_home () <> "" andalso not (null (#thy_map (mash_get ())))
6.292 + mash_home () <> "" andalso not (Graph.is_empty (#fact_graph (mash_get ())))
6.293
6.294 -fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts =
6.295 +fun parents_wrt facts fact_graph =
6.296 + let
6.297 + val facts =
6.298 + Symtab.empty
6.299 + |> fold (fn (_, th) => Symtab.update (Thm.get_name_hint th, ())) facts
6.300 + in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end
6.301 +
6.302 +fun mash_suggest_facts ctxt ({overlord, ...} : params) prover hyp_ts concl_t
6.303 + facts =
6.304 let
6.305 val thy = Proof_Context.theory_of ctxt
6.306 - val thy_map = #thy_map (mash_get ())
6.307 - val access = accessibility_of thy thy_map
6.308 + val fact_graph = #fact_graph (mash_get ())
6.309 + val parents = parents_wrt facts fact_graph
6.310 val feats = features_of thy General (concl_t :: hyp_ts)
6.311 - val suggs = mash_QUERY ctxt (access, feats)
6.312 + val suggs = mash_QUERY ctxt overlord (parents, feats)
6.313 in suggested_facts suggs facts end
6.314
6.315 -fun is_fact_in_thy_map thy_map fact =
6.316 - case AList.lookup (op =) thy_map (thy_name_of_fact fact) of
6.317 - SOME facts => member (op =) facts fact
6.318 - | NONE => false
6.319 +fun add_thys_for thy =
6.320 + let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
6.321 + add false thy #> fold (add true) (Theory.ancestors_of thy)
6.322 + end
6.323
6.324 -fun zip_facts news [] = news
6.325 - | zip_facts [] olds = olds
6.326 - | zip_facts (new :: news) (old :: olds) =
6.327 - if new = old then
6.328 - new :: zip_facts news olds
6.329 - else if member (op =) news old then
6.330 - old :: zip_facts (filter_out (curry (op =) old) news) olds
6.331 - else if member (op =) olds new then
6.332 - new :: zip_facts news (filter_out (curry (op =) new) olds)
6.333 - else
6.334 - new :: old :: zip_facts news olds
6.335 +fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
6.336 + let
6.337 + fun maybe_add_from from (accum as (parents, graph)) =
6.338 + (from :: parents, Graph.add_edge_acyclic (from, name) graph)
6.339 + handle Graph.CYCLES _ =>
6.340 + (trace_msg ctxt (fn () =>
6.341 + "Cycle between " ^ quote from ^ " and " ^ quote name); accum)
6.342 + | Graph.UNDEF _ =>
6.343 + (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum)
6.344 + val graph = graph |> Graph.new_node (name, ())
6.345 + val (parents, graph) = ([], graph) |> fold maybe_add_from parents
6.346 + val (deps, graph) = ([], graph) |> fold maybe_add_from deps
6.347 + in ((name, parents, feats, deps) :: upds, graph) end
6.348
6.349 -fun add_thy_map_from_thys [] old = old
6.350 - | add_thy_map_from_thys new old =
6.351 - let
6.352 - fun add_thy (thy, new_facts) =
6.353 - case AList.lookup (op =) old thy of
6.354 - SOME old_facts =>
6.355 - AList.update (op =) (thy, zip_facts old_facts new_facts)
6.356 - | NONE => cons (thy, new_facts)
6.357 - in old |> fold add_thy new end
6.358 -
6.359 -fun mash_learn_thy ctxt thy timeout =
6.360 +fun mash_learn_thy ctxt ({overlord, ...} : params) thy timeout =
6.361 let
6.362 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
6.363 val facts = all_facts_of thy css_table
6.364 - val {thy_map, ...} = mash_get ()
6.365 - fun is_old (_, th) = is_fact_in_thy_map thy_map (Thm.get_name_hint th)
6.366 - val (old_facts, new_facts) =
6.367 - facts |> List.partition is_old ||> sort (thm_ord o pairself snd)
6.368 + val {fact_graph, ...} = mash_get ()
6.369 + fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)
6.370 + val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)
6.371 in
6.372 if null new_facts then
6.373 ()
6.374 @@ -481,39 +504,49 @@
6.375 val ths = facts |> map snd
6.376 val all_names =
6.377 ths |> filter_out (is_likely_tautology orf is_too_meta)
6.378 - |> map Thm.get_name_hint
6.379 - fun do_fact ((_, (_, status)), th) (prevs, upds) =
6.380 + |> map (rpair () o Thm.get_name_hint)
6.381 + |> Symtab.make
6.382 + fun do_fact ((_, (_, status)), th) (parents, upds) =
6.383 let
6.384 val name = Thm.get_name_hint th
6.385 val feats = features_of thy status [prop_of th]
6.386 val deps = isabelle_dependencies_of all_names th
6.387 - val upd = (name, prevs, feats, deps)
6.388 + val upd = (name, parents, feats, deps)
6.389 in ([name], upd :: upds) end
6.390 - val parents = parent_facts thy thy_map
6.391 - val (_, upds) = (parents, []) |> fold do_fact new_facts
6.392 - val new_thy_map = new_facts |> thy_map_from_facts
6.393 - fun trans {dirty_thys, thy_map} =
6.394 - (mash_ADD ctxt (rev upds);
6.395 - {dirty_thys = dirty_thys,
6.396 - thy_map = thy_map |> add_thy_map_from_thys new_thy_map})
6.397 + val parents = parents_wrt facts fact_graph
6.398 + val (_, upds) = (parents, []) |> fold do_fact new_facts ||> rev
6.399 + fun trans {thys, fact_graph} =
6.400 + let
6.401 + val mash_INIT_or_ADD =
6.402 + if Graph.is_empty fact_graph then mash_INIT else mash_ADD
6.403 + val (upds, fact_graph) =
6.404 + ([], fact_graph) |> fold (update_fact_graph ctxt) upds
6.405 + in
6.406 + (mash_INIT_or_ADD ctxt overlord (rev upds);
6.407 + {thys = thys |> add_thys_for thy,
6.408 + fact_graph = fact_graph})
6.409 + end
6.410 in mash_map trans end
6.411 end
6.412
6.413 -fun mash_learn_proof ctxt thy t ths =
6.414 - mash_map (fn state as {dirty_thys, thy_map} =>
6.415 - let val deps = ths |> map Thm.get_name_hint in
6.416 - if forall (is_fact_in_thy_map thy_map) deps then
6.417 +fun mash_learn_proof ctxt ({overlord, ...} : params) t used_ths facts =
6.418 + let
6.419 + val thy = Proof_Context.theory_of ctxt
6.420 + val name = ATP_Util.timestamp () (* should be fairly fresh *)
6.421 + val feats = features_of thy General [t]
6.422 + val deps = used_ths |> map Thm.get_name_hint
6.423 + in
6.424 + mash_map (fn {thys, fact_graph} =>
6.425 let
6.426 - val fact = ATP_Util.timestamp () (* should be fairly fresh *)
6.427 - val access = accessibility_of thy thy_map
6.428 - val feats = features_of thy General [t]
6.429 + val parents = parents_wrt facts fact_graph
6.430 + val upds = [(name, parents, feats, deps)]
6.431 + val (upds, fact_graph) =
6.432 + ([], fact_graph) |> fold (update_fact_graph ctxt) upds
6.433 in
6.434 - mash_ADD ctxt [(fact, access, feats, deps)];
6.435 - {dirty_thys = dirty_thys, thy_map = thy_map}
6.436 - end
6.437 - else
6.438 - state
6.439 - end)
6.440 + mash_ADD ctxt overlord upds;
6.441 + {thys = thys, fact_graph = fact_graph}
6.442 + end)
6.443 + end
6.444
6.445 fun relevant_facts ctxt (params as {fact_filter, ...}) prover max_facts
6.446 ({add, only, ...} : fact_override) hyp_ts concl_t facts =
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200
7.3 @@ -13,7 +13,7 @@
7.4 val parse_time_option : string -> string -> Time.time option
7.5 val subgoal_count : Proof.state -> int
7.6 val reserved_isar_keyword_table : unit -> unit Symtab.table
7.7 - val thms_in_proof : string list option -> thm -> string list
7.8 + val thms_in_proof : unit Symtab.table option -> thm -> string list
7.9 end;
7.10
7.11 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
7.12 @@ -63,28 +63,24 @@
7.13 fun fold_body_thms thm_name f =
7.14 let
7.15 fun app n (PBody {thms, ...}) =
7.16 - thms |> fold (fn (_, (name, prop, body)) => fn x =>
7.17 - let
7.18 - val body' = Future.join body
7.19 - val n' =
7.20 - n + (if name = "" orelse
7.21 - (* uncommon case where the proved theorem occurs twice
7.22 - (e.g., "Transitive_Closure.trancl_into_trancl") *)
7.23 - (n = 1 andalso name = thm_name) then
7.24 - 0
7.25 - else
7.26 - 1)
7.27 - val x' = x |> n' <= 1 ? app n' body'
7.28 - in (x' |> n = 1 ? f (name, prop, body')) end)
7.29 + thms |> fold (fn (_, (name, _, body)) => fn accum =>
7.30 + let
7.31 + (* The second disjunct caters for the uncommon case where the proved
7.32 + theorem occurs in its own proof (e.g.,
7.33 + "Transitive_Closure.trancl_into_trancl"). *)
7.34 + val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
7.35 + val accum =
7.36 + accum |> (if n = 1 andalso not no_name then f name else I)
7.37 + val n = n + (if no_name then 0 else 1)
7.38 + in accum |> (if n <= 1 then app n (Future.join body) else I) end)
7.39 in fold (app 0) end
7.40
7.41 fun thms_in_proof all_names th =
7.42 let
7.43 - val is_name_ok =
7.44 + val collect =
7.45 case all_names of
7.46 - SOME names => member (op =) names
7.47 - | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
7.48 - fun collect (s, _, _) = is_name_ok s ? insert (op =) s
7.49 + SOME names => (fn s => Symtab.defined names s ? insert (op =) s)
7.50 + | NONE => insert (op =)
7.51 val names =
7.52 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
7.53 in names end