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 @@ -107,15 +107,21 @@
1.4 handle TYPE _ => @{prop True}
1.5 end
1.6
1.7 +fun all_non_tautological_facts_of thy css_table =
1.8 + Sledgehammer_Fact.all_facts_of thy css_table
1.9 + |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology orf
1.10 + Sledgehammer_Filter_MaSh.is_too_meta) o snd)
1.11 +
1.12 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
1.13 let
1.14 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
1.15 - val type_enc = type_enc |> type_enc_from_string Strict
1.16 - |> adjust_type_enc format
1.17 + val type_enc =
1.18 + type_enc |> type_enc_from_string Strict
1.19 + |> adjust_type_enc format
1.20 val mono = not (is_type_enc_polymorphic type_enc)
1.21 val path = file_name |> Path.explode
1.22 val _ = File.write path ""
1.23 - val facts = Sledgehammer_Fact.all_facts_of thy css_table
1.24 + val facts = all_non_tautological_facts_of thy css_table
1.25 val atp_problem =
1.26 facts
1.27 |> map (fn ((_, loc), 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 @@ -16,9 +16,10 @@
2.4 structure MaSh_Eval : MASH_EVAL =
2.5 struct
2.6
2.7 +open Sledgehammer_Fact
2.8 open Sledgehammer_Filter_MaSh
2.9
2.10 -val isarN = "Isa"
2.11 +val isarN = "Isar"
2.12 val iterN = "Iter"
2.13 val mashN = "MaSh"
2.14 val meshN = "Mesh"
2.15 @@ -34,8 +35,11 @@
2.16 val path = file_name |> Path.explode
2.17 val lines = path |> File.read_lines
2.18 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
2.19 - val facts = all_non_tautological_facts_of thy css_table
2.20 - val all_names = facts |> map (Thm.get_name_hint o snd)
2.21 + val facts = all_facts_of thy css_table
2.22 + val all_names =
2.23 + facts |> map snd
2.24 + |> filter_out (is_likely_tautology orf is_too_meta)
2.25 + |> map Thm.get_name_hint
2.26 val iter_ok = Unsynchronized.ref 0
2.27 val mash_ok = Unsynchronized.ref 0
2.28 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 @@ -37,16 +37,16 @@
3.4 val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
3.5 val _ = File.append path s
3.6 in [fact] end
3.7 - val thy_facts =
3.8 - all_non_tautological_facts_of thy Termtab.empty
3.9 + val thy_map =
3.10 + all_facts_of thy Termtab.empty
3.11 |> not include_thy ? filter_out (has_thy thy o snd)
3.12 - |> thy_facts_from_thms
3.13 + |> thy_map_from_facts
3.14 fun do_thy facts =
3.15 let
3.16 val thy = thy_of_fact thy (hd facts)
3.17 - val parents = parent_facts thy thy_facts
3.18 + val parents = parent_facts thy thy_map
3.19 in fold do_fact facts parents; () end
3.20 - in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end
3.21 + in fold_rev (fn (_, facts) => K (do_thy facts)) thy_map () end
3.22
3.23 fun generate_features ctxt thy include_thy file_name =
3.24 let
3.25 @@ -54,7 +54,7 @@
3.26 val _ = File.write path ""
3.27 val css_table = clasimpset_rule_table_of ctxt
3.28 val facts =
3.29 - all_non_tautological_facts_of thy css_table
3.30 + all_facts_of thy css_table
3.31 |> not include_thy ? filter_out (has_thy thy o snd)
3.32 fun do_fact ((_, (_, status)), th) =
3.33 let
3.34 @@ -69,10 +69,12 @@
3.35 val path = file_name |> Path.explode
3.36 val _ = File.write path ""
3.37 val ths =
3.38 - all_non_tautological_facts_of thy Termtab.empty
3.39 + all_facts_of thy Termtab.empty
3.40 |> not include_thy ? filter_out (has_thy thy o snd)
3.41 |> map snd
3.42 - val all_names = ths |> map Thm.get_name_hint
3.43 + val all_names =
3.44 + ths |> filter_out (is_likely_tautology orf is_too_meta)
3.45 + |> map Thm.get_name_hint
3.46 fun do_thm th =
3.47 let
3.48 val name = Thm.get_name_hint th
3.49 @@ -87,10 +89,12 @@
3.50 val path = file_name |> Path.explode
3.51 val _ = File.write path ""
3.52 val facts =
3.53 - all_non_tautological_facts_of thy Termtab.empty
3.54 + all_facts_of thy Termtab.empty
3.55 |> not include_thy ? filter_out (has_thy thy o snd)
3.56 val ths = facts |> map snd
3.57 - val all_names = ths |> map Thm.get_name_hint
3.58 + val all_names =
3.59 + ths |> filter_out (is_likely_tautology orf is_too_meta)
3.60 + |> map Thm.get_name_hint
3.61 fun is_dep dep (_, th) = Thm.get_name_hint th = dep
3.62 fun add_isa_dep facts dep accum =
3.63 if exists (is_dep dep) accum then
3.64 @@ -133,12 +137,14 @@
3.65 val path = file_name |> Path.explode
3.66 val _ = File.write path ""
3.67 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
3.68 - val facts = all_non_tautological_facts_of thy css_table
3.69 + val facts = all_facts_of thy css_table
3.70 val (new_facts, old_facts) =
3.71 facts |> List.partition (has_thy thy o snd)
3.72 |>> sort (thm_ord o pairself snd)
3.73 val ths = facts |> map snd
3.74 - val all_names = ths |> map Thm.get_name_hint
3.75 + val all_names =
3.76 + ths |> filter_out (is_likely_tautology orf is_too_meta)
3.77 + |> map Thm.get_name_hint
3.78 fun do_fact ((_, (_, status)), th) prevs =
3.79 let
3.80 val name = Thm.get_name_hint th
3.81 @@ -152,8 +158,8 @@
3.82 escape_metas deps ^ "\n"
3.83 val _ = File.append path (query ^ update)
3.84 in [name] end
3.85 - val thy_facts = old_facts |> thy_facts_from_thms
3.86 - val parents = parent_facts thy thy_facts
3.87 + val thy_map = old_facts |> thy_map_from_facts
3.88 + val parents = parent_facts thy thy_map
3.89 in fold do_fact new_facts parents; () end
3.90
3.91 fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
3.92 @@ -162,7 +168,7 @@
3.93 val path = file_name |> Path.explode
3.94 val _ = File.write path ""
3.95 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
3.96 - val facts = all_non_tautological_facts_of thy css_table
3.97 + val facts = all_facts_of thy css_table
3.98 val (new_facts, old_facts) =
3.99 facts |> List.partition (has_thy thy o snd)
3.100 |>> sort (thm_ord o pairself snd)
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
4.3 @@ -26,13 +26,13 @@
4.4 val extract_query : string -> string * string list
4.5 val suggested_facts : string list -> fact list -> fact list
4.6 val mesh_facts : int -> (fact list * int option) list -> fact list
4.7 - val all_non_tautological_facts_of :
4.8 - theory -> status Termtab.table -> fact list
4.9 + val is_likely_tautology : thm -> bool
4.10 + val is_too_meta : thm -> bool
4.11 val theory_ord : theory * theory -> order
4.12 val thm_ord : thm * thm -> order
4.13 - val thy_facts_from_thms : fact list -> string list Symtab.table
4.14 + val thy_map_from_facts : fact list -> (string * string list) list
4.15 val has_thy : theory -> thm -> bool
4.16 - val parent_facts : theory -> string list Symtab.table -> string list
4.17 + val parent_facts : theory -> (string * string list) list -> string list
4.18 val features_of : theory -> status -> term list -> string list
4.19 val isabelle_dependencies_of : string list -> thm -> string list
4.20 val goal_of_thm : theory -> thm -> thm
4.21 @@ -49,7 +49,6 @@
4.22 val mash_suggest_facts :
4.23 Proof.context -> params -> string -> term list -> term -> fact list
4.24 -> fact list
4.25 - val mash_can_learn_thy : Proof.context -> theory -> bool
4.26 val mash_learn_thy : Proof.context -> theory -> real -> unit
4.27 val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit
4.28 val relevant_facts :
4.29 @@ -103,14 +102,13 @@
4.30
4.31 val escape_meta = String.translate meta_char
4.32 val escape_metas = map escape_meta #> space_implode " "
4.33 -val unescape_meta = unmeta_chars [] o String.explode
4.34 -val unescape_metas = map unescape_meta o space_explode " "
4.35 +val unescape_meta = String.explode #> unmeta_chars []
4.36 +val unescape_metas =
4.37 + space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
4.38
4.39 -val explode_suggs =
4.40 - space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
4.41 fun extract_query line =
4.42 case space_explode ":" line of
4.43 - [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs)
4.44 + [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
4.45 | _ => ("", [])
4.46
4.47 fun find_suggested facts sugg =
4.48 @@ -230,37 +228,37 @@
4.49 null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso
4.50 not (Thm.eq_thm_prop (@{thm ext}, th))
4.51
4.52 -fun is_too_meta thy th =
4.53 - fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
4.54 -
4.55 -fun all_non_tautological_facts_of thy css_table =
4.56 - all_facts_of thy css_table
4.57 - |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
4.58 +(* ### FIXME: optimize *)
4.59 +fun is_too_meta th =
4.60 + fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th))
4.61 + <> @{typ bool}
4.62
4.63 fun theory_ord p =
4.64 - if Theory.eq_thy p then EQUAL
4.65 - else if Theory.subthy p then LESS
4.66 - else if Theory.subthy (swap p) then GREATER
4.67 - else EQUAL
4.68 + if Theory.eq_thy p then
4.69 + EQUAL
4.70 + else if Theory.subthy p then
4.71 + LESS
4.72 + else if Theory.subthy (swap p) then
4.73 + GREATER
4.74 + else case int_ord (pairself (length o Theory.ancestors_of) p) of
4.75 + EQUAL => string_ord (pairself Context.theory_name p)
4.76 + | order => order
4.77
4.78 val thm_ord = theory_ord o pairself theory_of_thm
4.79
4.80 -(* ### FIXME: optimize *)
4.81 -fun thy_facts_from_thms ths =
4.82 - ths |> map (snd #> `(theory_of_thm #> Context.theory_name))
4.83 - |> AList.group (op =)
4.84 - |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
4.85 - o hd o snd))
4.86 - |> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint))
4.87 - |> Symtab.make
4.88 +fun thy_map_from_facts ths =
4.89 + ths |> sort (thm_ord o swap o pairself snd)
4.90 + |> map (snd #> `(theory_of_thm #> Context.theory_name))
4.91 + |> AList.coalesce (op =)
4.92 + |> map (apsnd (map Thm.get_name_hint))
4.93
4.94 fun has_thy thy th =
4.95 Context.theory_name thy = Context.theory_name (theory_of_thm th)
4.96
4.97 -fun parent_facts thy thy_facts =
4.98 +fun parent_facts thy thy_map =
4.99 let
4.100 fun add_last thy =
4.101 - case Symtab.lookup thy_facts (Context.theory_name thy) of
4.102 + case AList.lookup (op =) thy_map (Context.theory_name thy) of
4.103 SOME (last_fact :: _) => insert (op =) last_fact
4.104 | _ => add_parent thy
4.105 and add_parent thy = fold add_last (Theory.parents_of thy)
4.106 @@ -312,10 +310,10 @@
4.107 Sledgehammer_Provers.Normal (hd provers)
4.108 in prover params (K (K (K ""))) problem end
4.109
4.110 -fun accessibility_of thy thy_facts =
4.111 - case Symtab.lookup thy_facts (Context.theory_name thy) of
4.112 +fun accessibility_of thy thy_map =
4.113 + case AList.lookup (op =) thy_map (Context.theory_name thy) of
4.114 SOME (fact :: _) => [fact]
4.115 - | _ => parent_facts thy thy_facts
4.116 + | _ => parent_facts thy thy_map
4.117
4.118 val thy_name_of_fact = hd o Long_Name.explode
4.119
4.120 @@ -376,12 +374,10 @@
4.121 (*** High-level communication with MaSh ***)
4.122
4.123 type mash_state =
4.124 - {dirty_thys : unit Symtab.table,
4.125 - thy_facts : string list Symtab.table}
4.126 + {dirty_thys : string list,
4.127 + thy_map : (string * string list) list}
4.128
4.129 -val empty_state =
4.130 - {dirty_thys = Symtab.empty,
4.131 - thy_facts = Symtab.empty}
4.132 +val empty_state = {dirty_thys = [], thy_map = []}
4.133
4.134 local
4.135
4.136 @@ -392,28 +388,25 @@
4.137 case try File.read_lines path of
4.138 SOME (dirty_line :: facts_lines) =>
4.139 let
4.140 - fun dirty_thys_of_line line =
4.141 - Symtab.make (line |> unescape_metas |> map (rpair ()))
4.142 fun add_facts_line line =
4.143 case unescape_metas line of
4.144 - thy :: facts => Symtab.update_new (thy, facts)
4.145 + thy :: facts => cons (thy, facts)
4.146 | _ => I (* shouldn't happen *)
4.147 in
4.148 - {dirty_thys = dirty_thys_of_line dirty_line,
4.149 - thy_facts = fold add_facts_line facts_lines Symtab.empty}
4.150 + {dirty_thys = unescape_metas dirty_line,
4.151 + thy_map = fold_rev add_facts_line facts_lines []}
4.152 end
4.153 | _ => empty_state)
4.154 end
4.155
4.156 -fun mash_save ({dirty_thys, thy_facts} : mash_state) =
4.157 +fun mash_save ({dirty_thys, thy_map} : mash_state) =
4.158 let
4.159 val path = mash_state_path ()
4.160 - val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n"
4.161 + val dirty_line = escape_metas dirty_thys ^ "\n"
4.162 fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n"
4.163 in
4.164 File.write path dirty_line;
4.165 - Symtab.fold (fn thy_fact => fn () =>
4.166 - File.append path (fact_line_for thy_fact)) thy_facts ()
4.167 + List.app (File.append path o fact_line_for) thy_map
4.168 end
4.169
4.170 val global_state =
4.171 @@ -434,22 +427,19 @@
4.172 end
4.173
4.174 fun mash_can_suggest_facts (_ : Proof.context) =
4.175 - not (Symtab.is_empty (#thy_facts (mash_get ())))
4.176 + mash_home () <> "" andalso not (null (#thy_map (mash_get ())))
4.177
4.178 fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts =
4.179 let
4.180 val thy = Proof_Context.theory_of ctxt
4.181 - val thy_facts = #thy_facts (mash_get ())
4.182 - val access = accessibility_of thy thy_facts
4.183 + val thy_map = #thy_map (mash_get ())
4.184 + val access = accessibility_of thy thy_map
4.185 val feats = features_of thy General (concl_t :: hyp_ts)
4.186 val suggs = mash_QUERY ctxt (access, feats)
4.187 in suggested_facts suggs facts end
4.188
4.189 -fun mash_can_learn_thy (_ : Proof.context) thy =
4.190 - not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy))
4.191 -
4.192 -fun is_fact_in_thy_facts thy_facts fact =
4.193 - case Symtab.lookup thy_facts (thy_name_of_fact fact) of
4.194 +fun is_fact_in_thy_map thy_map fact =
4.195 + case AList.lookup (op =) thy_map (thy_name_of_fact fact) of
4.196 SOME facts => member (op =) facts fact
4.197 | NONE => false
4.198
4.199 @@ -465,20 +455,22 @@
4.200 else
4.201 new :: old :: zip_facts news olds
4.202
4.203 -fun add_thy_facts_from_thys new old =
4.204 - let
4.205 - fun add_thy (thy, new_facts) =
4.206 - case Symtab.lookup old thy of
4.207 - SOME old_facts => Symtab.update (thy, zip_facts old_facts new_facts)
4.208 - | NONE => Symtab.update_new (thy, new_facts)
4.209 - in old |> Symtab.fold add_thy new end
4.210 +fun add_thy_map_from_thys [] old = old
4.211 + | add_thy_map_from_thys new old =
4.212 + let
4.213 + fun add_thy (thy, new_facts) =
4.214 + case AList.lookup (op =) old thy of
4.215 + SOME old_facts =>
4.216 + AList.update (op =) (thy, zip_facts old_facts new_facts)
4.217 + | NONE => cons (thy, new_facts)
4.218 + in old |> fold add_thy new end
4.219
4.220 fun mash_learn_thy ctxt thy timeout =
4.221 let
4.222 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
4.223 - val facts = all_non_tautological_facts_of thy css_table
4.224 - val {thy_facts, ...} = mash_get ()
4.225 - fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th)
4.226 + val facts = all_facts_of thy css_table
4.227 + val {thy_map, ...} = mash_get ()
4.228 + fun is_old (_, th) = is_fact_in_thy_map thy_map (Thm.get_name_hint th)
4.229 val (old_facts, new_facts) =
4.230 facts |> List.partition is_old ||> sort (thm_ord o pairself snd)
4.231 in
4.232 @@ -487,7 +479,9 @@
4.233 else
4.234 let
4.235 val ths = facts |> map snd
4.236 - val all_names = ths |> map Thm.get_name_hint
4.237 + val all_names =
4.238 + ths |> filter_out (is_likely_tautology orf is_too_meta)
4.239 + |> map Thm.get_name_hint
4.240 fun do_fact ((_, (_, status)), th) (prevs, upds) =
4.241 let
4.242 val name = Thm.get_name_hint th
4.243 @@ -495,27 +489,27 @@
4.244 val deps = isabelle_dependencies_of all_names th
4.245 val upd = (name, prevs, feats, deps)
4.246 in ([name], upd :: upds) end
4.247 - val parents = parent_facts thy thy_facts
4.248 + val parents = parent_facts thy thy_map
4.249 val (_, upds) = (parents, []) |> fold do_fact new_facts
4.250 - val new_thy_facts = new_facts |> thy_facts_from_thms
4.251 - fun trans {dirty_thys, thy_facts} =
4.252 + val new_thy_map = new_facts |> thy_map_from_facts
4.253 + fun trans {dirty_thys, thy_map} =
4.254 (mash_ADD ctxt (rev upds);
4.255 {dirty_thys = dirty_thys,
4.256 - thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts})
4.257 + thy_map = thy_map |> add_thy_map_from_thys new_thy_map})
4.258 in mash_map trans end
4.259 end
4.260
4.261 fun mash_learn_proof ctxt thy t ths =
4.262 - mash_map (fn state as {dirty_thys, thy_facts} =>
4.263 + mash_map (fn state as {dirty_thys, thy_map} =>
4.264 let val deps = ths |> map Thm.get_name_hint in
4.265 - if forall (is_fact_in_thy_facts thy_facts) deps then
4.266 + if forall (is_fact_in_thy_map thy_map) deps then
4.267 let
4.268 val fact = ATP_Util.timestamp () (* should be fairly fresh *)
4.269 - val access = accessibility_of thy thy_facts
4.270 + val access = accessibility_of thy thy_map
4.271 val feats = features_of thy General [t]
4.272 in
4.273 mash_ADD ctxt [(fact, access, feats, deps)];
4.274 - {dirty_thys = dirty_thys, thy_facts = thy_facts}
4.275 + {dirty_thys = dirty_thys, thy_map = thy_map}
4.276 end
4.277 else
4.278 state
4.279 @@ -534,7 +528,7 @@
4.280 val fact_filter =
4.281 case fact_filter of
4.282 SOME ff => ff
4.283 - | NONE => if mash_home () = "" then iterN else meshN
4.284 + | NONE => if mash_can_suggest_facts ctxt then meshN else iterN
4.285 val add_ths = Attrib.eval_thms ctxt add
4.286 fun prepend_facts ths accepts =
4.287 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @