1.1 --- a/src/HOL/IsaMakefile Wed Jul 11 13:54:37 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Jul 11 13:59:39 2012 +0200
1.3 @@ -1147,8 +1147,10 @@
1.4 $(LOG)/HOL-TPTP.gz: $(OUT)/HOL \
1.5 TPTP/ATP_Problem_Import.thy \
1.6 TPTP/ATP_Theory_Export.thy \
1.7 + TPTP/MaSh_Export.thy \
1.8 + TPTP/MaSh_Import.thy \
1.9 + TPTP/ROOT.ML \
1.10 TPTP/THF_Arith.thy \
1.11 - TPTP/ROOT.ML \
1.12 TPTP/TPTP_Parser.thy \
1.13 TPTP/TPTP_Parser/ml_yacc_lib.ML \
1.14 TPTP/TPTP_Parser/tptp_interpret.ML \
1.15 @@ -1159,6 +1161,8 @@
1.16 TPTP/TPTP_Parser_Test.thy \
1.17 TPTP/atp_problem_import.ML \
1.18 TPTP/atp_theory_export.ML \
1.19 + TPTP/mash_export.ML \
1.20 + TPTP/mash_import.ML \
1.21 TPTP/sledgehammer_tactics.ML
1.22 @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
1.23
2.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 11 13:54:37 2012 +0200
2.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 11 13:59:39 2012 +0200
2.3 @@ -16,52 +16,14 @@
2.4
2.5 ML {*
2.6 val do_it = false; (* switch to "true" to generate the files *)
2.7 -val thy = @{theory Complex_Main};
2.8 +val thy = @{theory};
2.9 val ctxt = @{context}
2.10 *}
2.11
2.12 -
2.13 -(* MaSh *)
2.14 -
2.15 -ML {*
2.16 -if do_it then
2.17 - "/tmp/mash_sample_problem.out"
2.18 - |> generate_mash_problem_file_for_theory thy
2.19 -else
2.20 - ()
2.21 -*}
2.22 -
2.23 ML {*
2.24 if do_it then
2.25 - "/tmp/mash_accessibility.out"
2.26 - |> generate_mash_accessibility_file_for_theory thy false
2.27 -else
2.28 - ()
2.29 -*}
2.30 -
2.31 -ML {*
2.32 -if do_it then
2.33 - "/tmp/mash_features.out"
2.34 - |> generate_mash_feature_file_for_theory thy false
2.35 -else
2.36 - ()
2.37 -*}
2.38 -
2.39 -ML {*
2.40 -if do_it then
2.41 - "/tmp/mash_dependencies.out"
2.42 - |> generate_mash_dependency_file_for_theory thy false
2.43 -else
2.44 - ()
2.45 -*}
2.46 -
2.47 -
2.48 -(* TPTP/DFG *)
2.49 -
2.50 -ML {*
2.51 -if do_it then
2.52 "/tmp/infs_poly_guards_query_query.tptp"
2.53 - |> generate_tptp_inference_file_for_theory ctxt thy FOF
2.54 + |> generate_atp_inference_file_for_theory ctxt thy FOF
2.55 "poly_guards_query_query"
2.56 else
2.57 ()
2.58 @@ -70,7 +32,7 @@
2.59 ML {*
2.60 if do_it then
2.61 "/tmp/infs_poly_tags_query_query.tptp"
2.62 - |> generate_tptp_inference_file_for_theory ctxt thy FOF
2.63 + |> generate_atp_inference_file_for_theory ctxt thy FOF
2.64 "poly_tags_query_query"
2.65 else
2.66 ()
2.67 @@ -79,7 +41,7 @@
2.68 ML {*
2.69 if do_it then
2.70 "/tmp/axs_tc_native.dfg"
2.71 - |> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic)
2.72 + |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
2.73 "tc_native"
2.74 else
2.75 ()
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 13:59:39 2012 +0200
3.3 @@ -0,0 +1,48 @@
3.4 +(* Title: HOL/TPTP/MaSh_Export.thy
3.5 + Author: Jasmin Blanchette, TU Muenchen
3.6 +*)
3.7 +
3.8 +header {* MaSh Exporter *}
3.9 +
3.10 +theory MaSh_Export
3.11 +imports ATP_Theory_Export
3.12 +uses "mash_export.ML"
3.13 +begin
3.14 +
3.15 +sledgehammer_params [provers = e, max_relevant = 500]
3.16 +
3.17 +ML {*
3.18 +open MaSh_Export
3.19 +*}
3.20 +
3.21 +ML {*
3.22 +val do_it = false (* switch to "true" to generate the files *);
3.23 +val thy = @{theory List}
3.24 +*}
3.25 +
3.26 +ML {*
3.27 +if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
3.28 +else ()
3.29 +*}
3.30 +
3.31 +ML {*
3.32 +if do_it then generate_mash_commands thy "/tmp/mash_commands"
3.33 +else ()
3.34 +*}
3.35 +
3.36 +ML {*
3.37 +if do_it then generate_mash_features thy false "/tmp/mash_features"
3.38 +else ()
3.39 +*}
3.40 +
3.41 +ML {*
3.42 +if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
3.43 +else ()
3.44 +*}
3.45 +
3.46 +ML {*
3.47 +if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
3.48 +else ()
3.49 +*}
3.50 +
3.51 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 13:59:39 2012 +0200
4.3 @@ -0,0 +1,32 @@
4.4 +(* Title: HOL/TPTP/MaSh_Import.thy
4.5 + Author: Jasmin Blanchette, TU Muenchen
4.6 +*)
4.7 +
4.8 +header {* MaSh Importer *}
4.9 +
4.10 +theory MaSh_Import
4.11 +imports MaSh_Export
4.12 +uses "mash_import.ML"
4.13 +begin
4.14 +
4.15 +sledgehammer_params
4.16 + [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
4.17 + lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
4.18 +
4.19 +declare [[sledgehammer_instantiate_inducts]]
4.20 +
4.21 +ML {*
4.22 +open MaSh_Import
4.23 +*}
4.24 +
4.25 +ML {*
4.26 +val do_it = false (* switch to "true" to generate the files *);
4.27 +val thy = @{theory Nat}
4.28 +*}
4.29 +
4.30 +ML {*
4.31 +if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
4.32 +else ()
4.33 +*}
4.34 +
4.35 +end
5.1 --- a/src/HOL/TPTP/ROOT.ML Wed Jul 11 13:54:37 2012 +0200
5.2 +++ b/src/HOL/TPTP/ROOT.ML Wed Jul 11 13:59:39 2012 +0200
5.3 @@ -8,6 +8,7 @@
5.4
5.5 use_thys [
5.6 "ATP_Theory_Export",
5.7 + "MaSh_Import",
5.8 "TPTP_Interpret",
5.9 "THF_Arith"
5.10 ];
6.1 --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 13:54:37 2012 +0200
6.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 13:59:39 2012 +0200
6.3 @@ -2,68 +2,30 @@
6.4 Author: Jasmin Blanchette, TU Muenchen
6.5 Copyright 2011
6.6
6.7 -Export Isabelle theories as MaSh (Machine-learning for Sledgehammer) or as
6.8 -first-order TPTP inferences.
6.9 +Export Isabelle theories as first-order TPTP inferences.
6.10 *)
6.11
6.12 signature ATP_THEORY_EXPORT =
6.13 sig
6.14 type atp_format = ATP_Problem.atp_format
6.15 + type stature = Sledgehammer_Filter.stature
6.16
6.17 val theorems_mentioned_in_proof_term :
6.18 string list option -> thm -> string list
6.19 - val generate_mash_accessibility_file_for_theory :
6.20 - theory -> bool -> string -> unit
6.21 - val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit
6.22 - val generate_mash_dependency_file_for_theory :
6.23 - theory -> bool -> string -> unit
6.24 - val generate_mash_problem_file_for_theory : theory -> string -> unit
6.25 - val generate_tptp_inference_file_for_theory :
6.26 + val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list
6.27 + val generate_atp_inference_file_for_theory :
6.28 Proof.context -> theory -> atp_format -> string -> string -> unit
6.29 end;
6.30
6.31 -structure ATP_Theory_Export (* ### : ATP_THEORY_EXPORT *) =
6.32 +structure ATP_Theory_Export : ATP_THEORY_EXPORT =
6.33 struct
6.34
6.35 open ATP_Problem
6.36 open ATP_Proof
6.37 open ATP_Problem_Generate
6.38 open ATP_Systems
6.39 -open ATP_Util
6.40
6.41 -fun stringN_of_int 0 _ = ""
6.42 - | stringN_of_int k n =
6.43 - stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
6.44 -
6.45 -fun escape_meta_char c =
6.46 - if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
6.47 - c = #")" then
6.48 - String.str c
6.49 - else if c = #"'" then
6.50 - "~"
6.51 - else
6.52 - (* fixed width, in case more digits follow *)
6.53 - "\\" ^ stringN_of_int 3 (Char.ord c)
6.54 -val escape_meta = String.translate escape_meta_char
6.55 -
6.56 -val fact_name_of = escape_meta
6.57 -val thy_name_of = escape_meta
6.58 -val const_name_of = prefix const_prefix o escape_meta
6.59 -val type_name_of = prefix type_const_prefix o escape_meta
6.60 -val class_name_of = prefix class_prefix o escape_meta
6.61 -
6.62 -val thy_name_of_thm = theory_of_thm #> Context.theory_name
6.63 -
6.64 -fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
6.65 -
6.66 -fun facts_of thy =
6.67 - let val ctxt = Proof_Context.init_global thy in
6.68 - Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
6.69 - (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
6.70 - |> filter (curry (op =) @{typ bool} o fastype_of
6.71 - o Object_Logic.atomize_term thy o prop_of o snd)
6.72 - |> rev
6.73 - end
6.74 +val fact_name_of = prefix fact_prefix o ascii_of
6.75
6.76 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
6.77 fixes that seem to be missing over there; or maybe the two code portions are
6.78 @@ -95,215 +57,15 @@
6.79 fun collect (s, _, _) = is_name_ok s ? insert (op =) s
6.80 val names =
6.81 [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
6.82 - |> map fact_name_of
6.83 in names end
6.84
6.85 -fun raw_interesting_const_names thy =
6.86 +fun all_facts_of_theory thy =
6.87 let val ctxt = Proof_Context.init_global thy in
6.88 - Sledgehammer_Filter.const_names_in_fact thy
6.89 - (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN)
6.90 + Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
6.91 + (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
6.92 + |> rev (* try to restore the original order of facts, for MaSh *)
6.93 end
6.94
6.95 -fun interesting_const_names thy =
6.96 - raw_interesting_const_names thy
6.97 - #> map const_name_of
6.98 - #> sort_distinct string_ord
6.99 -
6.100 -fun interesting_type_and_class_names t =
6.101 - let
6.102 - val bad = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
6.103 - val add_classes =
6.104 - subtract (op =) @{sort type} #> map class_name_of #> union (op =)
6.105 - fun maybe_add_type (Type (s, Ts)) =
6.106 - (not (member (op =) bad s) ? insert (op =) (type_name_of s))
6.107 - #> fold maybe_add_type Ts
6.108 - | maybe_add_type (TFree (_, S)) = add_classes S
6.109 - | maybe_add_type (TVar (_, S)) = add_classes S
6.110 - in [] |> fold_types maybe_add_type t end
6.111 -
6.112 -fun theory_ord p =
6.113 - if Theory.eq_thy p then EQUAL
6.114 - else if Theory.subthy p then LESS
6.115 - else if Theory.subthy (swap p) then GREATER
6.116 - else EQUAL
6.117 -
6.118 -val thm_ord = theory_ord o pairself theory_of_thm
6.119 -
6.120 -fun parent_thms thy_ths thy =
6.121 - Theory.parents_of thy
6.122 - |> map (thy_name_of o Context.theory_name)
6.123 - |> map_filter (AList.lookup (op =) thy_ths)
6.124 - |> map List.last
6.125 - |> map (fact_name_of o Thm.get_name_hint)
6.126 -
6.127 -val thms_by_thy =
6.128 - map (snd #> `thy_name_of_thm)
6.129 - #> AList.group (op =)
6.130 - #> sort (int_ord
6.131 - o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd))
6.132 - #> map (apsnd (sort thm_ord))
6.133 -
6.134 -fun generate_mash_accessibility_file_for_theory thy include_thy file_name =
6.135 - let
6.136 - val path = file_name |> Path.explode
6.137 - val _ = File.write path ""
6.138 - fun do_thm th prevs =
6.139 - let
6.140 - val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
6.141 - val _ = File.append path s
6.142 - in [th] end
6.143 - val thy_ths =
6.144 - facts_of thy
6.145 - |> not include_thy ? filter_out (has_thy thy o snd)
6.146 - |> thms_by_thy
6.147 - fun do_thy ths =
6.148 - let
6.149 - val thy = theory_of_thm (hd ths)
6.150 - val parents = parent_thms thy_ths thy
6.151 - val ths = ths |> map (fact_name_of o Thm.get_name_hint)
6.152 - val _ = fold do_thm ths parents
6.153 - in () end
6.154 - val _ = List.app (do_thy o snd) thy_ths
6.155 - in () end
6.156 -
6.157 -fun has_bool @{typ bool} = true
6.158 - | has_bool (Type (_, Ts)) = exists has_bool Ts
6.159 - | has_bool _ = false
6.160 -
6.161 -fun has_fun (Type (@{type_name fun}, _)) = true
6.162 - | has_fun (Type (_, Ts)) = exists has_fun Ts
6.163 - | has_fun _ = false
6.164 -
6.165 -val is_conn = member (op =)
6.166 - [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
6.167 - @{const_name HOL.implies}, @{const_name Not},
6.168 - @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
6.169 - @{const_name HOL.eq}]
6.170 -
6.171 -val has_bool_arg_const =
6.172 - exists_Const (fn (c, T) =>
6.173 - not (is_conn c) andalso exists has_bool (binder_types T))
6.174 -
6.175 -fun higher_inst_const thy (c, T) =
6.176 - case binder_types T of
6.177 - [] => false
6.178 - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
6.179 -
6.180 -val binders = [@{const_name All}, @{const_name Ex}]
6.181 -
6.182 -fun is_fo_term thy t =
6.183 - let
6.184 - val t =
6.185 - t |> Envir.beta_eta_contract
6.186 - |> transform_elim_prop
6.187 - |> Object_Logic.atomize_term thy
6.188 - in
6.189 - Term.is_first_order binders t andalso
6.190 - not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
6.191 - | _ => false) t orelse
6.192 - has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
6.193 - end
6.194 -
6.195 -val is_skolem = String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix
6.196 -val is_abs = String.isSubstring Sledgehammer_Filter.pseudo_abs_name
6.197 -
6.198 -(* TODO: Add types, subterms *)
6.199 -fun features_of thy (status, th) =
6.200 - let val prop = Thm.prop_of th in
6.201 - interesting_const_names thy prop @
6.202 - interesting_type_and_class_names prop
6.203 - |> (fn feats =>
6.204 - case List.partition is_skolem feats of
6.205 - ([], feats) => feats
6.206 - | (_, feats) => "skolem" :: feats)
6.207 - |> (fn feats =>
6.208 - case List.partition is_abs feats of
6.209 - ([], feats) => feats
6.210 - | (_, feats) => "abs" :: feats)
6.211 - |> not (is_fo_term thy prop) ? cons "ho"
6.212 - |> (case status of
6.213 - General => I
6.214 - | Induction => cons "induction"
6.215 - | Intro => cons "intro"
6.216 - | Inductive => cons "inductive"
6.217 - | Elim => cons "elim"
6.218 - | Simp => cons "simp"
6.219 - | Def => cons "def")
6.220 - end
6.221 -
6.222 -fun generate_mash_feature_file_for_theory thy include_thy file_name =
6.223 - let
6.224 - val path = file_name |> Path.explode
6.225 - val _ = File.write path ""
6.226 - val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd)
6.227 - fun do_fact ((_, (_, status)), th) =
6.228 - let
6.229 - val name = Thm.get_name_hint th
6.230 - val feats = features_of thy (status, th)
6.231 - val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
6.232 - in File.append path s end
6.233 - val _ = List.app do_fact facts
6.234 - in () end
6.235 -
6.236 -val dependencies_of = theorems_mentioned_in_proof_term o SOME
6.237 -
6.238 -val known_tautologies =
6.239 - [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def},
6.240 - @{thm Bex_def}, @{thm If_def}]
6.241 -
6.242 -fun is_likely_tautology thy th =
6.243 - (member Thm.eq_thm_prop known_tautologies th orelse
6.244 - th |> prop_of |> raw_interesting_const_names thy
6.245 - |> forall (is_skolem orf is_abs)) andalso
6.246 - not (Thm.eq_thm_prop (@{thm ext}, th))
6.247 -
6.248 -fun generate_mash_dependency_file_for_theory thy include_thy file_name =
6.249 - let
6.250 - val path = file_name |> Path.explode
6.251 - val _ = File.write path ""
6.252 - val ths =
6.253 - facts_of thy |> not include_thy ? filter_out (has_thy thy o snd)
6.254 - |> map snd
6.255 - val all_names =
6.256 - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint
6.257 - fun do_thm th =
6.258 - let
6.259 - val name = Thm.get_name_hint th
6.260 - val deps = dependencies_of all_names th
6.261 - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
6.262 - in File.append path s end
6.263 - val _ = List.app do_thm ths
6.264 - in () end
6.265 -
6.266 -fun generate_mash_problem_file_for_theory thy file_name =
6.267 - let
6.268 - val path = file_name |> Path.explode
6.269 - val _ = File.write path ""
6.270 - val facts = facts_of thy
6.271 - val (new_facts, old_facts) =
6.272 - facts |> List.partition (has_thy thy o snd)
6.273 - |>> sort (thm_ord o pairself snd)
6.274 - val ths = facts |> map snd
6.275 - val all_names =
6.276 - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint
6.277 - fun do_fact ((_, (_, status)), th) prevs =
6.278 - let
6.279 - val name = Thm.get_name_hint th
6.280 - val feats = features_of thy (status, th)
6.281 - val deps = dependencies_of all_names th
6.282 - val th = fact_name_of name
6.283 - val s =
6.284 - th ^ ": " ^
6.285 - space_implode " " prevs ^ "; " ^
6.286 - space_implode " " feats ^ "; " ^
6.287 - space_implode " " deps ^ "\n"
6.288 - val _ = File.append path s
6.289 - in [th] end
6.290 - val thy_ths = old_facts |> thms_by_thy
6.291 - val parents = parent_thms thy_ths thy
6.292 - val _ = fold do_fact new_facts parents
6.293 - in () end
6.294 -
6.295 fun inference_term [] = NONE
6.296 | inference_term ss =
6.297 ATerm (("inference", []),
6.298 @@ -384,14 +146,14 @@
6.299 handle TYPE _ => @{prop True}
6.300 end
6.301
6.302 -fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
6.303 +fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
6.304 let
6.305 val type_enc = type_enc |> type_enc_from_string Strict
6.306 |> adjust_type_enc format
6.307 val mono = not (is_type_enc_polymorphic type_enc)
6.308 val path = file_name |> Path.explode
6.309 val _ = File.write path ""
6.310 - val facts = facts_of thy
6.311 + val facts = all_facts_of_theory thy
6.312 val atp_problem =
6.313 facts
6.314 |> map (fn ((_, loc), th) =>
6.315 @@ -404,12 +166,12 @@
6.316 atp_problem
6.317 |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
6.318 val ths = facts |> map snd
6.319 - val all_names =
6.320 - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint
6.321 + val all_names = ths |> map Thm.get_name_hint
6.322 val infers =
6.323 facts |> map (fn (_, th) =>
6.324 (fact_name_of (Thm.get_name_hint th),
6.325 - theorems_mentioned_in_proof_term (SOME all_names) th))
6.326 + th |> theorems_mentioned_in_proof_term (SOME all_names)
6.327 + |> map fact_name_of))
6.328 val all_atp_problem_names =
6.329 atp_problem |> maps (map ident_of_problem_line o snd)
6.330 val infers =
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 13:59:39 2012 +0200
7.3 @@ -0,0 +1,341 @@
7.4 +(* Title: HOL/TPTP/mash_export.ML
7.5 + Author: Jasmin Blanchette, TU Muenchen
7.6 + Copyright 2012
7.7 +
7.8 +Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
7.9 +*)
7.10 +
7.11 +signature MASH_EXPORT =
7.12 +sig
7.13 + type stature = ATP_Problem_Generate.stature
7.14 +
7.15 + val non_tautological_facts_of :
7.16 + theory -> (((unit -> string) * stature) * thm) list
7.17 + val theory_ord : theory * theory -> order
7.18 + val thm_ord : thm * thm -> order
7.19 + val dependencies_of : string list -> thm -> string list
7.20 + val goal_of_thm : thm -> thm
7.21 + val meng_paulson_facts :
7.22 + Proof.context -> string -> int -> real * real -> thm -> int
7.23 + -> (((unit -> string) * stature) * thm) list
7.24 + -> ((string * stature) * thm) list
7.25 + val generate_mash_accessibility : theory -> bool -> string -> unit
7.26 + val generate_mash_features : theory -> bool -> string -> unit
7.27 + val generate_mash_dependencies : theory -> bool -> string -> unit
7.28 + val generate_mash_commands : theory -> string -> unit
7.29 + val generate_meng_paulson_suggestions :
7.30 + Proof.context -> theory -> string -> unit
7.31 +end;
7.32 +
7.33 +structure MaSh_Export : MASH_EXPORT =
7.34 +struct
7.35 +
7.36 +open ATP_Problem_Generate
7.37 +open ATP_Util
7.38 +
7.39 +fun stringN_of_int 0 _ = ""
7.40 + | stringN_of_int k n =
7.41 + stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
7.42 +
7.43 +fun escape_meta_char c =
7.44 + if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
7.45 + c = #")" orelse c = #"," then
7.46 + String.str c
7.47 + else
7.48 + (* fixed width, in case more digits follow *)
7.49 + "\\" ^ stringN_of_int 3 (Char.ord c)
7.50 +
7.51 +val escape_meta = String.translate escape_meta_char
7.52 +
7.53 +val thy_prefix = "y_"
7.54 +
7.55 +val fact_name_of = escape_meta
7.56 +val thy_name_of = prefix thy_prefix o escape_meta
7.57 +val const_name_of = prefix const_prefix o escape_meta
7.58 +val type_name_of = prefix type_const_prefix o escape_meta
7.59 +val class_name_of = prefix class_prefix o escape_meta
7.60 +
7.61 +val thy_name_of_thm = theory_of_thm #> Context.theory_name
7.62 +
7.63 +local
7.64 +
7.65 +fun has_bool @{typ bool} = true
7.66 + | has_bool (Type (_, Ts)) = exists has_bool Ts
7.67 + | has_bool _ = false
7.68 +
7.69 +fun has_fun (Type (@{type_name fun}, _)) = true
7.70 + | has_fun (Type (_, Ts)) = exists has_fun Ts
7.71 + | has_fun _ = false
7.72 +
7.73 +val is_conn = member (op =)
7.74 + [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
7.75 + @{const_name HOL.implies}, @{const_name Not},
7.76 + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
7.77 + @{const_name HOL.eq}]
7.78 +
7.79 +val has_bool_arg_const =
7.80 + exists_Const (fn (c, T) =>
7.81 + not (is_conn c) andalso exists has_bool (binder_types T))
7.82 +
7.83 +fun higher_inst_const thy (c, T) =
7.84 + case binder_types T of
7.85 + [] => false
7.86 + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
7.87 +
7.88 +val binders = [@{const_name All}, @{const_name Ex}]
7.89 +
7.90 +in
7.91 +
7.92 +fun is_fo_term thy t =
7.93 + let
7.94 + val t =
7.95 + t |> Envir.beta_eta_contract
7.96 + |> transform_elim_prop
7.97 + |> Object_Logic.atomize_term thy
7.98 + in
7.99 + Term.is_first_order binders t andalso
7.100 + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
7.101 + | _ => false) t orelse
7.102 + has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
7.103 + end
7.104 +
7.105 +end
7.106 +
7.107 +fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
7.108 + let
7.109 + val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
7.110 + val bad_consts = atp_widely_irrelevant_consts
7.111 + val add_classes =
7.112 + subtract (op =) @{sort type} #> map class_name_of #> union (op =)
7.113 + fun do_add_type (Type (s, Ts)) =
7.114 + (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
7.115 + #> fold do_add_type Ts
7.116 + | do_add_type (TFree (_, S)) = add_classes S
7.117 + | do_add_type (TVar (_, S)) = add_classes S
7.118 + fun add_type T = type_max_depth >= 0 ? do_add_type T
7.119 + fun mk_app s args =
7.120 + if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
7.121 + else s
7.122 + fun patternify ~1 _ = ""
7.123 + | patternify depth t =
7.124 + case strip_comb t of
7.125 + (Const (s, _), args) =>
7.126 + mk_app (const_name_of s) (map (patternify (depth - 1)) args)
7.127 + | _ => ""
7.128 + fun add_term_patterns ~1 _ = I
7.129 + | add_term_patterns depth t =
7.130 + insert (op =) (patternify depth t)
7.131 + #> add_term_patterns (depth - 1) t
7.132 + val add_term = add_term_patterns term_max_depth
7.133 + fun add_patterns t =
7.134 + let val (head, args) = strip_comb t in
7.135 + (case head of
7.136 + Const (s, T) =>
7.137 + not (member (op =) bad_consts s) ? (add_term t #> add_type T)
7.138 + | Free (_, T) => add_type T
7.139 + | Var (_, T) => add_type T
7.140 + | Abs (_, T, body) => add_type T #> add_patterns body
7.141 + | _ => I)
7.142 + #> fold add_patterns args
7.143 + end
7.144 + in [] |> add_patterns t |> sort string_ord end
7.145 +
7.146 +fun is_likely_tautology th =
7.147 + null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
7.148 + not (Thm.eq_thm_prop (@{thm ext}, th))
7.149 +
7.150 +fun is_too_meta thy th =
7.151 + fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
7.152 +
7.153 +fun non_tautological_facts_of thy =
7.154 + all_facts_of_theory thy
7.155 + |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
7.156 +
7.157 +fun theory_ord p =
7.158 + if Theory.eq_thy p then EQUAL
7.159 + else if Theory.subthy p then LESS
7.160 + else if Theory.subthy (swap p) then GREATER
7.161 + else EQUAL
7.162 +
7.163 +val thm_ord = theory_ord o pairself theory_of_thm
7.164 +
7.165 +fun thms_by_thy ths =
7.166 + ths |> map (snd #> `thy_name_of_thm)
7.167 + |> AList.group (op =)
7.168 + |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
7.169 + o hd o snd))
7.170 + |> map (apsnd (sort thm_ord))
7.171 +
7.172 +fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
7.173 +
7.174 +fun parent_thms thy_ths thy =
7.175 + Theory.parents_of thy
7.176 + |> map Context.theory_name
7.177 + |> map_filter (AList.lookup (op =) thy_ths)
7.178 + |> map List.last
7.179 + |> map (fact_name_of o Thm.get_name_hint)
7.180 +
7.181 +fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
7.182 +
7.183 +val max_depth = 1
7.184 +
7.185 +(* TODO: Generate type classes for types? *)
7.186 +fun features_of thy (status, th) =
7.187 + let val t = Thm.prop_of th in
7.188 + thy_name_of (thy_name_of_thm th) ::
7.189 + interesting_terms_types_and_classes max_depth max_depth t
7.190 + |> not (has_no_lambdas t) ? cons "lambdas"
7.191 + |> exists_Const is_exists t ? cons "skolems"
7.192 + |> not (is_fo_term thy t) ? cons "ho"
7.193 + |> (case status of
7.194 + General => I
7.195 + | Induction => cons "induction"
7.196 + | Intro => cons "intro"
7.197 + | Inductive => cons "inductive"
7.198 + | Elim => cons "elim"
7.199 + | Simp => cons "simp"
7.200 + | Def => cons "def")
7.201 + end
7.202 +
7.203 +val dependencies_of =
7.204 + map fact_name_of oo theorems_mentioned_in_proof_term o SOME
7.205 +
7.206 +val freezeT = Type.legacy_freeze_type
7.207 +
7.208 +fun freeze (t $ u) = freeze t $ freeze u
7.209 + | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
7.210 + | freeze (Var ((s, _), T)) = Free (s, freezeT T)
7.211 + | freeze (Const (s, T)) = Const (s, freezeT T)
7.212 + | freeze (Free (s, T)) = Free (s, freezeT T)
7.213 + | freeze t = t
7.214 +
7.215 +val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
7.216 +
7.217 +fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds
7.218 + goal i =
7.219 + let
7.220 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
7.221 + val is_built_in_const =
7.222 + Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
7.223 + val relevance_fudge =
7.224 + Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
7.225 + val relevance_override = {add = [], del = [], only = false}
7.226 + in
7.227 + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
7.228 + max_relevant is_built_in_const relevance_fudge relevance_override []
7.229 + hyp_ts concl_t
7.230 + end
7.231 +
7.232 +fun generate_mash_accessibility thy include_thy file_name =
7.233 + let
7.234 + val path = file_name |> Path.explode
7.235 + val _ = File.write path ""
7.236 + fun do_thm th prevs =
7.237 + let
7.238 + val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
7.239 + val _ = File.append path s
7.240 + in [th] end
7.241 + val thy_ths =
7.242 + non_tautological_facts_of thy
7.243 + |> not include_thy ? filter_out (has_thy thy o snd)
7.244 + |> thms_by_thy
7.245 + fun do_thy ths =
7.246 + let
7.247 + val thy = theory_of_thm (hd ths)
7.248 + val parents = parent_thms thy_ths thy
7.249 + val ths = ths |> map (fact_name_of o Thm.get_name_hint)
7.250 + in fold do_thm ths parents; () end
7.251 + in List.app (do_thy o snd) thy_ths end
7.252 +
7.253 +fun generate_mash_features thy include_thy file_name =
7.254 + let
7.255 + val path = file_name |> Path.explode
7.256 + val _ = File.write path ""
7.257 + val facts =
7.258 + non_tautological_facts_of thy
7.259 + |> not include_thy ? filter_out (has_thy thy o snd)
7.260 + fun do_fact ((_, (_, status)), th) =
7.261 + let
7.262 + val name = Thm.get_name_hint th
7.263 + val feats = features_of thy (status, th)
7.264 + val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
7.265 + in File.append path s end
7.266 + in List.app do_fact facts end
7.267 +
7.268 +fun generate_mash_dependencies thy include_thy file_name =
7.269 + let
7.270 + val path = file_name |> Path.explode
7.271 + val _ = File.write path ""
7.272 + val ths =
7.273 + non_tautological_facts_of thy
7.274 + |> not include_thy ? filter_out (has_thy thy o snd)
7.275 + |> map snd
7.276 + val all_names = ths |> map Thm.get_name_hint
7.277 + fun do_thm th =
7.278 + let
7.279 + val name = Thm.get_name_hint th
7.280 + val deps = dependencies_of all_names th
7.281 + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
7.282 + in File.append path s end
7.283 + in List.app do_thm ths end
7.284 +
7.285 +fun generate_mash_commands thy file_name =
7.286 + let
7.287 + val path = file_name |> Path.explode
7.288 + val _ = File.write path ""
7.289 + val facts = non_tautological_facts_of thy
7.290 + val (new_facts, old_facts) =
7.291 + facts |> List.partition (has_thy thy o snd)
7.292 + |>> sort (thm_ord o pairself snd)
7.293 + val ths = facts |> map snd
7.294 + val all_names = ths |> map Thm.get_name_hint
7.295 + fun do_fact ((_, (_, status)), th) prevs =
7.296 + let
7.297 + val name = Thm.get_name_hint th
7.298 + val feats = features_of thy (status, th)
7.299 + val deps = dependencies_of all_names th
7.300 + val kind = Thm.legacy_get_kind th
7.301 + val name = fact_name_of name
7.302 + val core =
7.303 + name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats
7.304 + val query = if kind <> "" then "? " ^ core ^ "\n" else ""
7.305 + val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n"
7.306 + val _ = File.append path (query ^ update)
7.307 + in [name] end
7.308 + val thy_ths = old_facts |> thms_by_thy
7.309 + val parents = parent_thms thy_ths thy
7.310 + in fold do_fact new_facts parents; () end
7.311 +
7.312 +fun generate_meng_paulson_suggestions ctxt thy file_name =
7.313 + let
7.314 + val {provers, max_relevant, relevance_thresholds, ...} =
7.315 + Sledgehammer_Isar.default_params ctxt []
7.316 + val prover_name = hd provers
7.317 + val path = file_name |> Path.explode
7.318 + val _ = File.write path ""
7.319 + val facts = non_tautological_facts_of thy
7.320 + val (new_facts, old_facts) =
7.321 + facts |> List.partition (has_thy thy o snd)
7.322 + |>> sort (thm_ord o pairself snd)
7.323 + val i = 1
7.324 + fun do_fact (fact as (_, th)) old_facts =
7.325 + let
7.326 + val name = Thm.get_name_hint th
7.327 + val goal = goal_of_thm th
7.328 + val kind = Thm.legacy_get_kind th
7.329 + val _ =
7.330 + if kind <> "" then
7.331 + let
7.332 + val suggs =
7.333 + old_facts
7.334 + |> meng_paulson_facts ctxt prover_name (the max_relevant)
7.335 + relevance_thresholds goal i
7.336 + |> map (fact_name_of o Thm.get_name_hint o snd)
7.337 + val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
7.338 + in File.append path s end
7.339 + else
7.340 + ()
7.341 + in fact :: old_facts end
7.342 + in fold do_fact new_facts old_facts; () end
7.343 +
7.344 +end;
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 13:59:39 2012 +0200
8.3 @@ -0,0 +1,163 @@
8.4 +(* Title: HOL/TPTP/mash_import.ML
8.5 + Author: Jasmin Blanchette, TU Muenchen
8.6 + Copyright 2012
8.7 +
8.8 +Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and
8.9 +evaluate them.
8.10 +*)
8.11 +
8.12 +signature MASH_IMPORT =
8.13 +sig
8.14 + val import_and_evaluate_mash_suggestions :
8.15 + Proof.context -> theory -> string -> unit
8.16 +end;
8.17 +
8.18 +structure MaSh_Import : MASH_IMPORT =
8.19 +struct
8.20 +
8.21 +open MaSh_Export
8.22 +
8.23 +val unescape_meta =
8.24 + let
8.25 + fun un accum [] = String.implode (rev accum)
8.26 + | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
8.27 + (case Int.fromString (String.implode [d1, d2, d3]) of
8.28 + SOME n => un (Char.chr n :: accum) cs
8.29 + | NONE => "" (* error *))
8.30 + | un _ (#"\\" :: _) = "" (* error *)
8.31 + | un accum (c :: cs) = un (c :: accum) cs
8.32 + in un [] o String.explode end
8.33 +
8.34 +val of_fact_name = unescape_meta
8.35 +
8.36 +val depN = "Dependencies"
8.37 +val mengN = "Meng & Paulson"
8.38 +val mashN = "MaSh"
8.39 +val meng_mashN = "M&P+MaSh"
8.40 +
8.41 +val max_relevant_slack = 2
8.42 +
8.43 +fun import_and_evaluate_mash_suggestions ctxt thy file_name =
8.44 + let
8.45 + val params as {provers, max_relevant, relevance_thresholds,
8.46 + slice, type_enc, lam_trans, timeout, ...} =
8.47 + Sledgehammer_Isar.default_params ctxt []
8.48 + val prover_name = hd provers
8.49 + val path = file_name |> Path.explode
8.50 + val lines = path |> File.read_lines
8.51 + val facts = non_tautological_facts_of thy
8.52 + val all_names = facts |> map (Thm.get_name_hint o snd)
8.53 + val i = 1
8.54 + val meng_ok = Unsynchronized.ref 0
8.55 + val mash_ok = Unsynchronized.ref 0
8.56 + val meng_mash_ok = Unsynchronized.ref 0
8.57 + val dep_ok = Unsynchronized.ref 0
8.58 + fun find_sugg facts sugg =
8.59 + find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
8.60 + fun sugg_facts hyp_ts concl_t facts =
8.61 + map_filter (find_sugg facts o of_fact_name)
8.62 + #> take (max_relevant_slack * the max_relevant)
8.63 + #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
8.64 + #> map (apfst (apfst (fn name => name ())))
8.65 + fun meng_mash_facts fs1 fs2 =
8.66 + let
8.67 + val fact_eq = (op =) o pairself fst
8.68 + fun score_in f fs =
8.69 + case find_index (curry fact_eq f) fs of
8.70 + ~1 => length fs
8.71 + | j => j
8.72 + fun score_of f = score_in f fs1 + score_in f fs2
8.73 + in
8.74 + union fact_eq fs1 fs2
8.75 + |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
8.76 + |> take (the max_relevant)
8.77 + end
8.78 + fun with_index facts s =
8.79 + (find_index (fn ((s', _), _) => s = s') facts + 1, s)
8.80 + fun index_string (j, s) = s ^ "@" ^ string_of_int j
8.81 + fun str_of_res label facts {outcome, run_time, used_facts, ...} =
8.82 + " " ^ label ^ ": " ^
8.83 + (if is_none outcome then
8.84 + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
8.85 + (used_facts |> map (with_index facts o fst)
8.86 + |> sort (int_ord o pairself fst)
8.87 + |> map index_string
8.88 + |> space_implode " ") ^
8.89 + (if length facts < the max_relevant then
8.90 + " (of " ^ string_of_int (length facts) ^ ")"
8.91 + else
8.92 + "")
8.93 + else
8.94 + "Failure: " ^
8.95 + (facts |> map (fst o fst)
8.96 + |> tag_list 1
8.97 + |> map index_string
8.98 + |> space_implode " "))
8.99 + fun run_sh ok heading facts goal =
8.100 + let
8.101 + val problem =
8.102 + {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
8.103 + facts = facts |> take (the max_relevant)
8.104 + |> map Sledgehammer_Provers.Untranslated_Fact}
8.105 + val prover =
8.106 + Sledgehammer_Run.get_minimizing_prover ctxt
8.107 + Sledgehammer_Provers.Normal prover_name
8.108 + val res as {outcome, ...} = prover params (K (K (K ""))) problem
8.109 + val _ = if is_none outcome then ok := !ok + 1 else ()
8.110 + in str_of_res heading facts res end
8.111 + fun solve_goal j name suggs =
8.112 + let
8.113 + val name = of_fact_name name
8.114 + val th =
8.115 + case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
8.116 + SOME (_, th) => th
8.117 + | NONE => error ("No fact called \"" ^ name ^ "\"")
8.118 + val deps = dependencies_of all_names th
8.119 + val goal = goal_of_thm th
8.120 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
8.121 + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
8.122 + val deps_facts = sugg_facts hyp_ts concl_t facts deps
8.123 + val meng_facts =
8.124 + meng_paulson_facts ctxt prover_name
8.125 + (max_relevant_slack * the max_relevant) relevance_thresholds goal
8.126 + i facts
8.127 + val mash_facts = sugg_facts hyp_ts concl_t facts suggs
8.128 + val meng_mash_facts = meng_mash_facts meng_facts mash_facts
8.129 + val meng_s = run_sh meng_ok mengN meng_facts goal
8.130 + val mash_s = run_sh mash_ok mashN mash_facts goal
8.131 + val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal
8.132 + val dep_s = run_sh dep_ok depN deps_facts goal
8.133 + in
8.134 + ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s,
8.135 + dep_s]
8.136 + |> cat_lines |> tracing
8.137 + end
8.138 + val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
8.139 + fun do_line (j, line) =
8.140 + case space_explode ":" line of
8.141 + [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs)
8.142 + | _ => ()
8.143 + fun total_of heading ok n =
8.144 + " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
8.145 + Real.fmt (StringCvt.FIX (SOME 1))
8.146 + (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
8.147 + val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
8.148 + val params =
8.149 + [prover_name, string_of_int (the max_relevant) ^ " facts",
8.150 + "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
8.151 + the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
8.152 + "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
8.153 + val n = length lines
8.154 + in
8.155 + tracing " * * *";
8.156 + tracing ("Options: " ^ commas params);
8.157 + List.app do_line (tag_list 1 lines);
8.158 + ["Successes (of " ^ string_of_int n ^ " goals)",
8.159 + total_of mengN meng_ok n,
8.160 + total_of mashN mash_ok n,
8.161 + total_of meng_mashN meng_mash_ok n,
8.162 + total_of depN dep_ok n]
8.163 + |> cat_lines |> tracing
8.164 + end
8.165 +
8.166 +end;
9.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 13:54:37 2012 +0200
9.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 13:59:39 2012 +0200
9.3 @@ -86,6 +86,7 @@
9.4 val unproxify_const : string -> string
9.5 val new_skolem_var_name_from_const : string -> string
9.6 val atp_irrelevant_consts : string list
9.7 + val atp_widely_irrelevant_consts : string list
9.8 val atp_schematic_consts_of : term -> typ list Symtab.table
9.9 val is_type_enc_higher_order : type_enc -> bool
9.10 val is_type_enc_polymorphic : type_enc -> bool
9.11 @@ -93,6 +94,7 @@
9.12 val is_type_enc_sound : type_enc -> bool
9.13 val type_enc_from_string : strictness -> string -> type_enc
9.14 val adjust_type_enc : atp_format -> type_enc -> type_enc
9.15 + val has_no_lambdas : term -> bool
9.16 val mk_aconns :
9.17 connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
9.18 val unmangled_const : string -> string * (string, 'b) ho_term list
9.19 @@ -399,7 +401,7 @@
9.20 @{const_name conj}, @{const_name disj}, @{const_name implies},
9.21 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
9.22
9.23 -val atp_monomorph_bad_consts =
9.24 +val atp_widely_irrelevant_consts =
9.25 atp_irrelevant_consts @
9.26 (* These are ignored anyway by the relevance filter (unless they appear in
9.27 higher-order places) but not by the monomorphizer. *)
9.28 @@ -411,7 +413,7 @@
9.29 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
9.30 val add_schematic_consts_of =
9.31 Term.fold_aterms (fn Const (x as (s, _)) =>
9.32 - not (member (op =) atp_monomorph_bad_consts s)
9.33 + not (member (op =) atp_widely_irrelevant_consts s)
9.34 ? add_schematic_const x
9.35 | _ => I)
9.36 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
9.37 @@ -701,22 +703,22 @@
9.38 (if is_type_enc_sound type_enc then Tags else Guards) stuff
9.39 | adjust_type_enc _ type_enc = type_enc
9.40
9.41 -fun is_fol_term t =
9.42 +fun has_no_lambdas t =
9.43 case t of
9.44 - @{const Not} $ t1 => is_fol_term t1
9.45 - | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'
9.46 - | Const (@{const_name All}, _) $ t1 => is_fol_term t1
9.47 - | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'
9.48 - | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1
9.49 - | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
9.50 - | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
9.51 - | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
9.52 + @{const Not} $ t1 => has_no_lambdas t1
9.53 + | Const (@{const_name All}, _) $ Abs (_, _, t') => has_no_lambdas t'
9.54 + | Const (@{const_name All}, _) $ t1 => has_no_lambdas t1
9.55 + | Const (@{const_name Ex}, _) $ Abs (_, _, t') => has_no_lambdas t'
9.56 + | Const (@{const_name Ex}, _) $ t1 => has_no_lambdas t1
9.57 + | @{const HOL.conj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
9.58 + | @{const HOL.disj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
9.59 + | @{const HOL.implies} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2
9.60 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
9.61 - is_fol_term t1 andalso is_fol_term t2
9.62 + has_no_lambdas t1 andalso has_no_lambdas t2
9.63 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
9.64
9.65 fun simple_translate_lambdas do_lambdas ctxt t =
9.66 - if is_fol_term t then
9.67 + if has_no_lambdas t then
9.68 t
9.69 else
9.70 let
9.71 @@ -2494,8 +2496,7 @@
9.72 let
9.73 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
9.74 val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts
9.75 - val decl_lines =
9.76 - fold_rev (append o lines_for_sym_decls ctxt mono type_enc) syms []
9.77 + val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms
9.78 in mono_lines @ decl_lines end
9.79
9.80 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
10.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 11 13:54:37 2012 +0200
10.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 11 13:59:39 2012 +0200
10.3 @@ -213,7 +213,8 @@
10.4
10.5 (* E *)
10.6
10.7 -fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER)
10.8 +fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
10.9 +fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
10.10
10.11 val tstp_proof_delims =
10.12 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
10.13 @@ -289,23 +290,35 @@
10.14 else "")
10.15 end
10.16
10.17 +fun e_shell_level_argument full_proof =
10.18 + if is_new_e_version () then
10.19 + " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
10.20 + else
10.21 + ""
10.22 +
10.23 fun effective_e_selection_heuristic ctxt =
10.24 - if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
10.25 + if is_recent_e_version () then Config.get ctxt e_selection_heuristic
10.26 + else e_autoN
10.27
10.28 -fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO"
10.29 +fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
10.30
10.31 val e_config : atp_config =
10.32 {exec = (["E_HOME"], "eproof"),
10.33 required_vars = [],
10.34 arguments =
10.35 - fn ctxt => fn _ => fn heuristic => fn timeout =>
10.36 + fn ctxt => fn full_proof => fn heuristic => fn timeout =>
10.37 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
10.38 "--tstp-in --tstp-out --output-level=5 --silent " ^
10.39 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
10.40 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
10.41 "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
10.42 - "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
10.43 - proof_delims = tstp_proof_delims,
10.44 + "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
10.45 + e_shell_level_argument full_proof,
10.46 + proof_delims =
10.47 + (* work-around for bug in "epclextract" version 1.6 *)
10.48 + ("# SZS status Theorem\n# SZS output start Saturation.",
10.49 + "# SZS output end Saturation.") ::
10.50 + tstp_proof_delims,
10.51 known_failures =
10.52 [(TimedOut, "Failure: Resource limit exceeded (time)"),
10.53 (TimedOut, "time limit exceeded")] @
11.1 --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 13:54:37 2012 +0200
11.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 13:59:39 2012 +0200
11.3 @@ -131,7 +131,7 @@
11.4 fun type_instance thy T T' = Sign.typ_instance thy (T, T')
11.5 fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
11.6 fun type_intersect thy T T' =
11.7 - can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
11.8 + can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T'))
11.9 (Vartab.empty, 0)
11.10 val type_equiv = Sign.typ_equiv
11.11
11.12 @@ -192,6 +192,7 @@
11.13 | (k1, k2) =>
11.14 if k1 >= max orelse k2 >= max then max
11.15 else Int.min (max, Integer.pow k2 k1))
11.16 + | Type (@{type_name set}, [T']) => aux slack avoid (T' --> @{typ bool})
11.17 | @{typ prop} => 2
11.18 | @{typ bool} => 2 (* optimization *)
11.19 | @{typ nat} => 0 (* optimization *)
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 13:54:37 2012 +0200
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 13:59:39 2012 +0200
12.3 @@ -53,6 +53,10 @@
12.4 Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
12.5 -> thm list -> status Termtab.table
12.6 -> (((unit -> string) * stature) * thm) list
12.7 + val maybe_instantiate_inducts :
12.8 + Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
12.9 + -> (((unit -> string) * 'a) * thm) list
12.10 + val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
12.11 val nearly_all_facts :
12.12 Proof.context -> bool -> relevance_override -> thm list -> term list -> term
12.13 -> (((unit -> string) * stature) * thm) list
12.14 @@ -446,8 +450,15 @@
12.15 | _ => do_term false t
12.16 in do_formula pos end
12.17
12.18 -(*Inserts a dummy "constant" referring to the theory name, so that relevance
12.19 - takes the given theory into account.*)
12.20 +fun pconsts_in_fact thy is_built_in_const t =
12.21 + Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
12.22 + (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
12.23 + (SOME true) t) []
12.24 +
12.25 +val const_names_in_fact = map fst ooo pconsts_in_fact
12.26 +
12.27 +(* Inserts a dummy "constant" referring to the theory name, so that relevance
12.28 + takes the given theory into account. *)
12.29 fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
12.30 : relevance_fudge) thy_name t =
12.31 if exists (curry (op <) 0.0) [theory_const_rel_weight,
12.32 @@ -459,6 +470,13 @@
12.33 fun theory_const_prop_of fudge th =
12.34 theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
12.35
12.36 +fun pair_consts_fact thy is_built_in_const fudge fact =
12.37 + case fact |> snd |> theory_const_prop_of fudge
12.38 + |> pconsts_in_fact thy is_built_in_const of
12.39 + [] => NONE
12.40 + | consts => SOME ((fact, consts), NONE)
12.41 +
12.42 +
12.43 (**** Constant / Type Frequencies ****)
12.44
12.45 (* A two-dimensional symbol table counts frequencies of constants. It's keyed
12.46 @@ -597,19 +615,6 @@
12.47 val res = rel_weight / (rel_weight + irrel_weight)
12.48 in if Real.isFinite res then res else 0.0 end
12.49
12.50 -fun pconsts_in_fact thy is_built_in_const t =
12.51 - Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
12.52 - (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
12.53 - (SOME true) t) []
12.54 -
12.55 -fun pair_consts_fact thy is_built_in_const fudge fact =
12.56 - case fact |> snd |> theory_const_prop_of fudge
12.57 - |> pconsts_in_fact thy is_built_in_const of
12.58 - [] => NONE
12.59 - | consts => SOME ((fact, consts), NONE)
12.60 -
12.61 -val const_names_in_fact = map fst ooo pconsts_in_fact
12.62 -
12.63 type annotated_thm =
12.64 (((unit -> string) * stature) * thm) * (string * ptype) list
12.65
12.66 @@ -958,19 +963,29 @@
12.67 fun external_frees t =
12.68 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
12.69
12.70 +fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
12.71 + if Config.get ctxt instantiate_inducts then
12.72 + let
12.73 + val thy = Proof_Context.theory_of ctxt
12.74 + val ind_stmt =
12.75 + (hyp_ts |> filter_out (null o external_frees), concl_t)
12.76 + |> Logic.list_implies |> Object_Logic.atomize_term thy
12.77 + val ind_stmt_xs = external_frees ind_stmt
12.78 + in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
12.79 + else
12.80 + I
12.81 +
12.82 +fun maybe_filter_no_atps ctxt =
12.83 + not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
12.84 +
12.85 fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
12.86 chained_ths hyp_ts concl_t =
12.87 if only andalso null add then
12.88 []
12.89 else
12.90 let
12.91 - val thy = Proof_Context.theory_of ctxt
12.92 val reserved = reserved_isar_keyword_table ()
12.93 val add_ths = Attrib.eval_thms ctxt add
12.94 - val ind_stmt =
12.95 - (hyp_ts |> filter_out (null o external_frees), concl_t)
12.96 - |> Logic.list_implies |> Object_Logic.atomize_term thy
12.97 - val ind_stmt_xs = external_frees ind_stmt
12.98 val css_table = clasimpset_rule_table_of ctxt
12.99 in
12.100 (if only then
12.101 @@ -978,10 +993,8 @@
12.102 o fact_from_ref ctxt reserved chained_ths css_table) add
12.103 else
12.104 all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
12.105 - |> Config.get ctxt instantiate_inducts
12.106 - ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
12.107 - |> (not (Config.get ctxt ignore_no_atp) andalso not only)
12.108 - ? filter_out (No_ATPs.member ctxt o snd)
12.109 + |> maybe_instantiate_inducts ctxt hyp_ts concl_t
12.110 + |> not only ? maybe_filter_no_atps ctxt
12.111 |> uniquify
12.112 end
12.113