1.1 --- a/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
1.2 +++ b/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
1.3 @@ -14,9 +14,9 @@
1.4 "Tools/Sledgehammer/sledgehammer_fact.ML"
1.5 "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
1.6 "Tools/Sledgehammer/sledgehammer_provers.ML"
1.7 + "Tools/Sledgehammer/sledgehammer_minimize.ML"
1.8 "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
1.9 "Tools/Sledgehammer/sledgehammer_filter.ML"
1.10 - "Tools/Sledgehammer/sledgehammer_minimize.ML"
1.11 "Tools/Sledgehammer/sledgehammer_run.ML"
1.12 "Tools/Sledgehammer/sledgehammer_isar.ML"
1.13 begin
2.1 --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
2.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
2.3 @@ -14,17 +14,19 @@
2.4 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
2.5
2.6 ML {*
2.7 +open Sledgehammer_Filter_MaSh
2.8 open MaSh_Export
2.9 *}
2.10
2.11 ML {*
2.12 val do_it = false (* switch to "true" to generate the files *);
2.13 -val thy = @{theory Nat}
2.14 +val thy = @{theory Nat};
2.15 +val params = Sledgehammer_Isar.default_params @{context} []
2.16 *}
2.17
2.18 ML {*
2.19 if do_it then
2.20 - generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
2.21 + generate_accessibility thy false "/tmp/mash_accessibility"
2.22 else
2.23 ()
2.24 *}
2.25 @@ -38,13 +40,6 @@
2.26
2.27 ML {*
2.28 if do_it then
2.29 - generate_accessibility thy false "/tmp/mash_accessibility"
2.30 -else
2.31 - ()
2.32 -*}
2.33 -
2.34 -ML {*
2.35 -if do_it then
2.36 generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
2.37 else
2.38 ()
2.39 @@ -52,7 +47,7 @@
2.40
2.41 ML {*
2.42 if do_it then
2.43 - generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
2.44 + generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies"
2.45 else
2.46 ()
2.47 *}
2.48 @@ -66,7 +61,7 @@
2.49
2.50 ML {*
2.51 if do_it then
2.52 - generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
2.53 + generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
2.54 else
2.55 ()
2.56 *}
3.1 --- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
3.2 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
3.3 @@ -16,13 +16,14 @@
3.4 *}
3.5
3.6 ML {*
3.7 -val do_it = true (* switch to "true" to generate the files *);
3.8 -val thy = @{theory List}
3.9 +val do_it = false (* switch to "true" to generate the files *);
3.10 +val thy = @{theory List};
3.11 +val params = Sledgehammer_Isar.default_params @{context} []
3.12 *}
3.13
3.14 ML {*
3.15 if do_it then
3.16 - import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
3.17 + import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list"
3.18 else
3.19 ()
3.20 *}
4.1 --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
4.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
4.3 @@ -8,11 +8,7 @@
4.4 signature ATP_THEORY_EXPORT =
4.5 sig
4.6 type atp_format = ATP_Problem.atp_format
4.7 - type stature = Sledgehammer_Filter.stature
4.8
4.9 - val theorems_mentioned_in_proof_term :
4.10 - string list option -> thm -> string list
4.11 - val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list
4.12 val generate_atp_inference_file_for_theory :
4.13 Proof.context -> theory -> atp_format -> string -> string -> unit
4.14 end;
4.15 @@ -27,45 +23,6 @@
4.16
4.17 val fact_name_of = prefix fact_prefix o ascii_of
4.18
4.19 -(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
4.20 - fixes that seem to be missing over there; or maybe the two code portions are
4.21 - not doing the same? *)
4.22 -fun fold_body_thms thm_name f =
4.23 - let
4.24 - fun app n (PBody {thms, ...}) =
4.25 - thms |> fold (fn (_, (name, prop, body)) => fn x =>
4.26 - let
4.27 - val body' = Future.join body
4.28 - val n' =
4.29 - n + (if name = "" orelse
4.30 - (* uncommon case where the proved theorem occurs twice
4.31 - (e.g., "Transitive_Closure.trancl_into_trancl") *)
4.32 - (n = 1 andalso name = thm_name) then
4.33 - 0
4.34 - else
4.35 - 1)
4.36 - val x' = x |> n' <= 1 ? app n' body'
4.37 - in (x' |> n = 1 ? f (name, prop, body')) end)
4.38 - in fold (app 0) end
4.39 -
4.40 -fun theorems_mentioned_in_proof_term all_names th =
4.41 - let
4.42 - val is_name_ok =
4.43 - case all_names of
4.44 - SOME names => member (op =) names
4.45 - | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
4.46 - fun collect (s, _, _) = is_name_ok s ? insert (op =) s
4.47 - val names =
4.48 - [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
4.49 - in names end
4.50 -
4.51 -fun all_facts_of_theory thy =
4.52 - let val ctxt = Proof_Context.init_global thy in
4.53 - Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
4.54 - (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
4.55 - |> rev (* try to restore the original order of facts, for MaSh *)
4.56 - end
4.57 -
4.58 fun inference_term [] = NONE
4.59 | inference_term ss =
4.60 ATerm (("inference", []),
4.61 @@ -153,7 +110,7 @@
4.62 val mono = not (is_type_enc_polymorphic type_enc)
4.63 val path = file_name |> Path.explode
4.64 val _ = File.write path ""
4.65 - val facts = all_facts_of_theory thy
4.66 + val facts = Sledgehammer_Fact.all_facts_of thy
4.67 val atp_problem =
4.68 facts
4.69 |> map (fn ((_, loc), th) =>
4.70 @@ -170,7 +127,7 @@
4.71 val infers =
4.72 facts |> map (fn (_, th) =>
4.73 (fact_name_of (Thm.get_name_hint th),
4.74 - th |> theorems_mentioned_in_proof_term (SOME all_names)
4.75 + th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
4.76 |> map fact_name_of))
4.77 val all_atp_problem_names =
4.78 atp_problem |> maps (map ident_of_problem_line o snd)
5.1 --- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
5.2 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
5.3 @@ -7,348 +7,23 @@
5.4
5.5 signature MASH_EXPORT =
5.6 sig
5.7 - type stature = ATP_Problem_Generate.stature
5.8 - type prover_result = Sledgehammer_Provers.prover_result
5.9 + type params = Sledgehammer_Provers.params
5.10
5.11 - val non_tautological_facts_of :
5.12 - theory -> (((unit -> string) * stature) * thm) list
5.13 - val theory_ord : theory * theory -> order
5.14 - val thm_ord : thm * thm -> order
5.15 - val dependencies_of : string list -> thm -> string list
5.16 - val goal_of_thm : theory -> thm -> thm
5.17 - val meng_paulson_facts :
5.18 - Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
5.19 - -> ((string * stature) * thm) list
5.20 - val run_sledgehammer :
5.21 - Proof.context -> ((string * stature) * thm) list -> thm -> prover_result
5.22 - val generate_accessibility : theory -> bool -> string -> unit
5.23 - val generate_features : theory -> bool -> string -> unit
5.24 - val generate_isa_dependencies : theory -> bool -> string -> unit
5.25 - val generate_atp_dependencies :
5.26 - Proof.context -> theory -> bool -> string -> unit
5.27 val generate_commands : theory -> string -> unit
5.28 - val generate_meng_paulson_suggestions :
5.29 - Proof.context -> theory -> int -> string -> unit
5.30 + val generate_iter_suggestions :
5.31 + Proof.context -> params -> theory -> int -> string -> unit
5.32 end;
5.33
5.34 structure MaSh_Export : MASH_EXPORT =
5.35 struct
5.36
5.37 -open ATP_Util
5.38 -open ATP_Problem_Generate
5.39 -open ATP_Theory_Export
5.40 -
5.41 -type prover_result = Sledgehammer_Provers.prover_result
5.42 -
5.43 -fun stringN_of_int 0 _ = ""
5.44 - | stringN_of_int k n =
5.45 - stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
5.46 -
5.47 -fun escape_meta_char c =
5.48 - if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
5.49 - c = #")" orelse c = #"," then
5.50 - String.str c
5.51 - else
5.52 - (* fixed width, in case more digits follow *)
5.53 - "\\" ^ stringN_of_int 3 (Char.ord c)
5.54 -
5.55 -val escape_meta = String.translate escape_meta_char
5.56 -
5.57 -val thy_prefix = "y_"
5.58 -
5.59 -val fact_name_of = escape_meta
5.60 -val thy_name_of = prefix thy_prefix o escape_meta
5.61 -val const_name_of = prefix const_prefix o escape_meta
5.62 -val type_name_of = prefix type_const_prefix o escape_meta
5.63 -val class_name_of = prefix class_prefix o escape_meta
5.64 -
5.65 -val thy_name_of_thm = theory_of_thm #> Context.theory_name
5.66 -
5.67 -local
5.68 -
5.69 -fun has_bool @{typ bool} = true
5.70 - | has_bool (Type (_, Ts)) = exists has_bool Ts
5.71 - | has_bool _ = false
5.72 -
5.73 -fun has_fun (Type (@{type_name fun}, _)) = true
5.74 - | has_fun (Type (_, Ts)) = exists has_fun Ts
5.75 - | has_fun _ = false
5.76 -
5.77 -val is_conn = member (op =)
5.78 - [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
5.79 - @{const_name HOL.implies}, @{const_name Not},
5.80 - @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
5.81 - @{const_name HOL.eq}]
5.82 -
5.83 -val has_bool_arg_const =
5.84 - exists_Const (fn (c, T) =>
5.85 - not (is_conn c) andalso exists has_bool (binder_types T))
5.86 -
5.87 -fun higher_inst_const thy (c, T) =
5.88 - case binder_types T of
5.89 - [] => false
5.90 - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
5.91 -
5.92 -val binders = [@{const_name All}, @{const_name Ex}]
5.93 -
5.94 -in
5.95 -
5.96 -fun is_fo_term thy t =
5.97 - let
5.98 - val t =
5.99 - t |> Envir.beta_eta_contract
5.100 - |> transform_elim_prop
5.101 - |> Object_Logic.atomize_term thy
5.102 - in
5.103 - Term.is_first_order binders t andalso
5.104 - not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
5.105 - | _ => false) t orelse
5.106 - has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
5.107 - end
5.108 -
5.109 -end
5.110 -
5.111 -fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
5.112 - let
5.113 - val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
5.114 - val bad_consts = atp_widely_irrelevant_consts
5.115 - fun do_add_type (Type (s, Ts)) =
5.116 - (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
5.117 - #> fold do_add_type Ts
5.118 - | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
5.119 - | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
5.120 - fun add_type T = type_max_depth >= 0 ? do_add_type T
5.121 - fun mk_app s args =
5.122 - if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
5.123 - else s
5.124 - fun patternify ~1 _ = ""
5.125 - | patternify depth t =
5.126 - case strip_comb t of
5.127 - (Const (s, _), args) =>
5.128 - mk_app (const_name_of s) (map (patternify (depth - 1)) args)
5.129 - | _ => ""
5.130 - fun add_term_patterns ~1 _ = I
5.131 - | add_term_patterns depth t =
5.132 - insert (op =) (patternify depth t)
5.133 - #> add_term_patterns (depth - 1) t
5.134 - val add_term = add_term_patterns term_max_depth
5.135 - fun add_patterns t =
5.136 - let val (head, args) = strip_comb t in
5.137 - (case head of
5.138 - Const (s, T) =>
5.139 - not (member (op =) bad_consts s) ? (add_term t #> add_type T)
5.140 - | Free (_, T) => add_type T
5.141 - | Var (_, T) => add_type T
5.142 - | Abs (_, T, body) => add_type T #> add_patterns body
5.143 - | _ => I)
5.144 - #> fold add_patterns args
5.145 - end
5.146 - in [] |> add_patterns t |> sort string_ord end
5.147 -
5.148 -fun is_likely_tautology th =
5.149 - null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
5.150 - not (Thm.eq_thm_prop (@{thm ext}, th))
5.151 -
5.152 -fun is_too_meta thy th =
5.153 - fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
5.154 -
5.155 -fun non_tautological_facts_of thy =
5.156 - all_facts_of_theory thy
5.157 - |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
5.158 -
5.159 -fun theory_ord p =
5.160 - if Theory.eq_thy p then EQUAL
5.161 - else if Theory.subthy p then LESS
5.162 - else if Theory.subthy (swap p) then GREATER
5.163 - else EQUAL
5.164 -
5.165 -val thm_ord = theory_ord o pairself theory_of_thm
5.166 -
5.167 -fun thms_by_thy ths =
5.168 - ths |> map (snd #> `thy_name_of_thm)
5.169 - |> AList.group (op =)
5.170 - |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
5.171 - o hd o snd))
5.172 - |> map (apsnd (sort thm_ord))
5.173 -
5.174 -fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
5.175 -
5.176 -fun parent_thms thy_ths thy =
5.177 - Theory.parents_of thy
5.178 - |> map Context.theory_name
5.179 - |> map_filter (AList.lookup (op =) thy_ths)
5.180 - |> map List.last
5.181 - |> map (fact_name_of o Thm.get_name_hint)
5.182 -
5.183 -fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
5.184 -
5.185 -val max_depth = 1
5.186 -
5.187 -(* TODO: Generate type classes for types? *)
5.188 -fun features_of thy (status, th) =
5.189 - let val t = Thm.prop_of th in
5.190 - thy_name_of (thy_name_of_thm th) ::
5.191 - interesting_terms_types_and_classes max_depth max_depth t
5.192 - |> not (has_no_lambdas t) ? cons "lambdas"
5.193 - |> exists_Const is_exists t ? cons "skolems"
5.194 - |> not (is_fo_term thy t) ? cons "ho"
5.195 - |> (case status of
5.196 - General => I
5.197 - | Induction => cons "induction"
5.198 - | Intro => cons "intro"
5.199 - | Inductive => cons "inductive"
5.200 - | Elim => cons "elim"
5.201 - | Simp => cons "simp"
5.202 - | Def => cons "def")
5.203 - end
5.204 -
5.205 -fun dependencies_of all_facts =
5.206 - theorems_mentioned_in_proof_term (SOME all_facts)
5.207 - #> map fact_name_of
5.208 - #> sort string_ord
5.209 -
5.210 -val freezeT = Type.legacy_freeze_type
5.211 -
5.212 -fun freeze (t $ u) = freeze t $ freeze u
5.213 - | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
5.214 - | freeze (Var ((s, _), T)) = Free (s, freezeT T)
5.215 - | freeze (Const (s, T)) = Const (s, freezeT T)
5.216 - | freeze (Free (s, T)) = Free (s, freezeT T)
5.217 - | freeze t = t
5.218 -
5.219 -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
5.220 -
5.221 -fun meng_paulson_facts ctxt max_relevant goal =
5.222 - let
5.223 - val {provers, relevance_thresholds, ...} =
5.224 - Sledgehammer_Isar.default_params ctxt []
5.225 - val prover_name = hd provers
5.226 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
5.227 - val is_built_in_const =
5.228 - Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
5.229 - val relevance_fudge =
5.230 - Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
5.231 - val relevance_override = {add = [], del = [], only = false}
5.232 - in
5.233 - Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
5.234 - max_relevant is_built_in_const relevance_fudge relevance_override []
5.235 - hyp_ts concl_t
5.236 - end
5.237 -
5.238 -fun run_sledgehammer ctxt facts goal =
5.239 - let
5.240 - val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt []
5.241 - val problem =
5.242 - {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
5.243 - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
5.244 - val prover =
5.245 - Sledgehammer_Minimize.get_minimizing_prover ctxt
5.246 - Sledgehammer_Provers.Normal (hd provers)
5.247 - in prover params (K (K (K ""))) problem end
5.248 -
5.249 -fun generate_accessibility thy include_thy file_name =
5.250 - let
5.251 - val path = file_name |> Path.explode
5.252 - val _ = File.write path ""
5.253 - fun do_thm th prevs =
5.254 - let
5.255 - val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
5.256 - val _ = File.append path s
5.257 - in [th] end
5.258 - val thy_ths =
5.259 - non_tautological_facts_of thy
5.260 - |> not include_thy ? filter_out (has_thy thy o snd)
5.261 - |> thms_by_thy
5.262 - fun do_thy ths =
5.263 - let
5.264 - val thy = theory_of_thm (hd ths)
5.265 - val parents = parent_thms thy_ths thy
5.266 - val ths = ths |> map (fact_name_of o Thm.get_name_hint)
5.267 - in fold do_thm ths parents; () end
5.268 - in List.app (do_thy o snd) thy_ths end
5.269 -
5.270 -fun generate_features thy include_thy file_name =
5.271 - let
5.272 - val path = file_name |> Path.explode
5.273 - val _ = File.write path ""
5.274 - val facts =
5.275 - non_tautological_facts_of thy
5.276 - |> not include_thy ? filter_out (has_thy thy o snd)
5.277 - fun do_fact ((_, (_, status)), th) =
5.278 - let
5.279 - val name = Thm.get_name_hint th
5.280 - val feats = features_of thy (status, th)
5.281 - val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
5.282 - in File.append path s end
5.283 - in List.app do_fact facts end
5.284 -
5.285 -fun generate_isa_dependencies thy include_thy file_name =
5.286 - let
5.287 - val path = file_name |> Path.explode
5.288 - val _ = File.write path ""
5.289 - val ths =
5.290 - non_tautological_facts_of thy
5.291 - |> not include_thy ? filter_out (has_thy thy o snd)
5.292 - |> map snd
5.293 - val all_names = ths |> map Thm.get_name_hint
5.294 - fun do_thm th =
5.295 - let
5.296 - val name = Thm.get_name_hint th
5.297 - val deps = dependencies_of all_names th
5.298 - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
5.299 - in File.append path s end
5.300 - in List.app do_thm ths end
5.301 -
5.302 -fun generate_atp_dependencies ctxt thy include_thy file_name =
5.303 - let
5.304 - val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt []
5.305 - val path = file_name |> Path.explode
5.306 - val _ = File.write path ""
5.307 - val facts =
5.308 - non_tautological_facts_of thy
5.309 - |> not include_thy ? filter_out (has_thy thy o snd)
5.310 - val ths = facts |> map snd
5.311 - val all_names = ths |> map Thm.get_name_hint
5.312 - fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
5.313 - fun add_isa_dep facts dep accum =
5.314 - if exists (is_dep dep) accum then
5.315 - accum
5.316 - else case find_first (is_dep dep) facts of
5.317 - SOME ((name, status), th) => accum @ [((name (), status), th)]
5.318 - | NONE => accum (* shouldn't happen *)
5.319 - fun fix_name ((_, stature), th) =
5.320 - ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
5.321 - fun do_thm th =
5.322 - let
5.323 - val name = Thm.get_name_hint th
5.324 - val goal = goal_of_thm thy th
5.325 - val deps =
5.326 - case dependencies_of all_names th of
5.327 - [] => []
5.328 - | isa_dep as [_] => isa_dep (* can hardly beat that *)
5.329 - | isa_deps =>
5.330 - let
5.331 - val facts =
5.332 - facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
5.333 - val facts =
5.334 - facts |> meng_paulson_facts ctxt (the max_relevant) goal
5.335 - |> fold (add_isa_dep facts) isa_deps
5.336 - |> map fix_name
5.337 - in
5.338 - case run_sledgehammer ctxt facts goal of
5.339 - {outcome = NONE, used_facts, ...} =>
5.340 - used_facts |> map fst |> sort string_ord
5.341 - | _ => isa_deps
5.342 - end
5.343 - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
5.344 - in File.append path s end
5.345 - in List.app do_thm ths end
5.346 +open Sledgehammer_Filter_MaSh
5.347
5.348 fun generate_commands thy file_name =
5.349 let
5.350 val path = file_name |> Path.explode
5.351 val _ = File.write path ""
5.352 - val facts = non_tautological_facts_of thy
5.353 + val facts = all_non_tautological_facts_of thy
5.354 val (new_facts, old_facts) =
5.355 facts |> List.partition (has_thy thy o snd)
5.356 |>> sort (thm_ord o pairself snd)
5.357 @@ -358,7 +33,7 @@
5.358 let
5.359 val name = Thm.get_name_hint th
5.360 val feats = features_of thy (status, th)
5.361 - val deps = dependencies_of all_names th
5.362 + val deps = isabelle_dependencies_of all_names th
5.363 val kind = Thm.legacy_get_kind th
5.364 val name = fact_name_of name
5.365 val core =
5.366 @@ -371,11 +46,11 @@
5.367 val parents = parent_thms thy_ths thy
5.368 in fold do_fact new_facts parents; () end
5.369
5.370 -fun generate_meng_paulson_suggestions ctxt thy max_relevant file_name =
5.371 +fun generate_iter_suggestions ctxt params thy max_relevant file_name =
5.372 let
5.373 val path = file_name |> Path.explode
5.374 val _ = File.write path ""
5.375 - val facts = non_tautological_facts_of thy
5.376 + val facts = all_non_tautological_facts_of thy
5.377 val (new_facts, old_facts) =
5.378 facts |> List.partition (has_thy thy o snd)
5.379 |>> sort (thm_ord o pairself snd)
5.380 @@ -388,7 +63,7 @@
5.381 if kind <> "" then
5.382 let
5.383 val suggs =
5.384 - old_facts |> meng_paulson_facts ctxt max_relevant goal
5.385 + old_facts |> iter_facts ctxt params max_relevant goal
5.386 |> map (fact_name_of o fst o fst)
5.387 |> sort string_ord
5.388 val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
6.1 --- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
6.2 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
6.3 @@ -8,13 +8,16 @@
6.4
6.5 signature MASH_IMPORT =
6.6 sig
6.7 + type params = Sledgehammer_Provers.params
6.8 +
6.9 val import_and_evaluate_mash_suggestions :
6.10 - Proof.context -> theory -> string -> unit
6.11 + Proof.context -> params -> theory -> string -> unit
6.12 end;
6.13
6.14 structure MaSh_Import : MASH_IMPORT =
6.15 struct
6.16
6.17 +open Sledgehammer_Filter_MaSh
6.18 open MaSh_Export
6.19
6.20 val unescape_meta =
6.21 @@ -30,26 +33,26 @@
6.22
6.23 val of_fact_name = unescape_meta
6.24
6.25 -val depN = "Dependencies"
6.26 -val mengN = "Meng & Paulson"
6.27 +val isaN = "Isabelle"
6.28 +val iterN = "Iterative"
6.29 val mashN = "MaSh"
6.30 -val meng_mashN = "M&P+MaSh"
6.31 +val iter_mashN = "Iter+MaSh"
6.32
6.33 val max_relevant_slack = 2
6.34
6.35 -fun import_and_evaluate_mash_suggestions ctxt thy file_name =
6.36 +fun import_and_evaluate_mash_suggestions ctxt params thy file_name =
6.37 let
6.38 val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} =
6.39 Sledgehammer_Isar.default_params ctxt []
6.40 val prover_name = hd provers
6.41 val path = file_name |> Path.explode
6.42 val lines = path |> File.read_lines
6.43 - val facts = non_tautological_facts_of thy
6.44 + val facts = all_non_tautological_facts_of thy
6.45 val all_names = facts |> map (Thm.get_name_hint o snd)
6.46 - val meng_ok = Unsynchronized.ref 0
6.47 + val iter_ok = Unsynchronized.ref 0
6.48 val mash_ok = Unsynchronized.ref 0
6.49 - val meng_mash_ok = Unsynchronized.ref 0
6.50 - val dep_ok = Unsynchronized.ref 0
6.51 + val iter_mash_ok = Unsynchronized.ref 0
6.52 + val isa_ok = Unsynchronized.ref 0
6.53 fun find_sugg facts sugg =
6.54 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
6.55 fun sugg_facts hyp_ts concl_t facts =
6.56 @@ -57,7 +60,7 @@
6.57 #> take (max_relevant_slack * the max_relevant)
6.58 #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
6.59 #> map (apfst (apfst (fn name => name ())))
6.60 - fun meng_mash_facts fs1 fs2 =
6.61 + fun iter_mash_facts fs1 fs2 =
6.62 let
6.63 val fact_eq = (op =) o pairself fst
6.64 fun score_in f fs =
6.65 @@ -92,10 +95,10 @@
6.66 |> tag_list 1
6.67 |> map index_string
6.68 |> space_implode " "))
6.69 - fun run_sh ok heading facts goal =
6.70 + fun prove ok heading facts goal =
6.71 let
6.72 val facts = facts |> take (the max_relevant)
6.73 - val res as {outcome, ...} = run_sledgehammer ctxt facts goal
6.74 + val res as {outcome, ...} = run_prover ctxt params facts goal
6.75 val _ = if is_none outcome then ok := !ok + 1 else ()
6.76 in str_of_res heading facts res end
6.77 fun solve_goal j name suggs =
6.78 @@ -105,23 +108,23 @@
6.79 case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
6.80 SOME (_, th) => th
6.81 | NONE => error ("No fact called \"" ^ name ^ "\"")
6.82 - val deps = dependencies_of all_names th
6.83 + val isa_deps = isabelle_dependencies_of all_names th
6.84 val goal = goal_of_thm thy th
6.85 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
6.86 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
6.87 - val deps_facts = sugg_facts hyp_ts concl_t facts deps
6.88 - val meng_facts =
6.89 - meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal
6.90 - facts
6.91 + val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
6.92 + val iter_facts =
6.93 + iter_facts ctxt params (max_relevant_slack * the max_relevant) goal
6.94 + facts
6.95 val mash_facts = sugg_facts hyp_ts concl_t facts suggs
6.96 - val meng_mash_facts = meng_mash_facts meng_facts mash_facts
6.97 - val meng_s = run_sh meng_ok mengN meng_facts goal
6.98 - val mash_s = run_sh mash_ok mashN mash_facts goal
6.99 - val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal
6.100 - val dep_s = run_sh dep_ok depN deps_facts goal
6.101 + val iter_mash_facts = iter_mash_facts iter_facts mash_facts
6.102 + val iter_s = prove iter_ok iterN iter_facts goal
6.103 + val mash_s = prove mash_ok mashN mash_facts goal
6.104 + val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal
6.105 + val isa_s = prove isa_ok isaN isa_facts goal
6.106 in
6.107 - ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s,
6.108 - dep_s]
6.109 + ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s,
6.110 + isa_s]
6.111 |> cat_lines |> tracing
6.112 end
6.113 val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
6.114 @@ -145,10 +148,10 @@
6.115 tracing ("Options: " ^ commas options);
6.116 List.app do_line (tag_list 1 lines);
6.117 ["Successes (of " ^ string_of_int n ^ " goals)",
6.118 - total_of mengN meng_ok n,
6.119 + total_of iterN iter_ok n,
6.120 total_of mashN mash_ok n,
6.121 - total_of meng_mashN meng_mash_ok n,
6.122 - total_of depN dep_ok n]
6.123 + total_of iter_mashN iter_mash_ok n,
6.124 + total_of isaN isa_ok n]
6.125 |> cat_lines |> tracing
6.126 end
6.127
7.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
7.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
7.3 @@ -252,10 +252,6 @@
7.4 Other characters go to _nnn where nnn is the decimal ASCII code.*)
7.5 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
7.6
7.7 -fun stringN_of_int 0 _ = ""
7.8 - | stringN_of_int k n =
7.9 - stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
7.10 -
7.11 fun ascii_of_char c =
7.12 if Char.isAlphaNum c then
7.13 String.str c
8.1 --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
8.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
8.3 @@ -9,6 +9,7 @@
8.4 val timestamp : unit -> string
8.5 val hash_string : string -> int
8.6 val hash_term : term -> int
8.7 + val stringN_of_int : int -> int -> string
8.8 val strip_spaces : bool -> (char -> bool) -> string -> string
8.9 val strip_spaces_except_between_idents : string -> string
8.10 val nat_subscript : int -> string
8.11 @@ -65,6 +66,10 @@
8.12 fun hash_string s = Word.toInt (hashw_string (s, 0w0))
8.13 val hash_term = Word.toInt o hashw_term
8.14
8.15 +fun stringN_of_int 0 _ = ""
8.16 + | stringN_of_int k n =
8.17 + stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
8.18 +
8.19 fun strip_spaces skip_comments is_evil =
8.20 let
8.21 fun strip_c_style_comment [] accum = accum
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200
9.3 @@ -21,15 +21,16 @@
9.4 val fact_from_ref :
9.5 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
9.6 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
9.7 - val all_facts :
9.8 - Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
9.9 - -> thm list -> status Termtab.table
9.10 - -> (((unit -> string) * stature) * thm) list
9.11 val clasimpset_rule_table_of : Proof.context -> status Termtab.table
9.12 val maybe_instantiate_inducts :
9.13 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
9.14 -> (((unit -> string) * 'a) * thm) list
9.15 val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
9.16 + val all_facts :
9.17 + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
9.18 + -> thm list -> status Termtab.table
9.19 + -> (((unit -> string) * stature) * thm) list
9.20 + val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
9.21 val nearly_all_facts :
9.22 Proof.context -> bool -> relevance_override -> thm list -> term list -> term
9.23 -> (((unit -> string) * stature) * thm) list
9.24 @@ -240,77 +241,6 @@
9.25 (Term.add_vars t [] |> sort_wrt (fst o fst))
9.26 |> fst
9.27
9.28 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
9.29 - let
9.30 - val thy = Proof_Context.theory_of ctxt
9.31 - val global_facts = Global_Theory.facts_of thy
9.32 - val local_facts = Proof_Context.facts_of ctxt
9.33 - val named_locals = local_facts |> Facts.dest_static []
9.34 - val assms = Assumption.all_assms_of ctxt
9.35 - fun is_good_unnamed_local th =
9.36 - not (Thm.has_name_hint th) andalso
9.37 - forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
9.38 - val unnamed_locals =
9.39 - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
9.40 - |> filter is_good_unnamed_local |> map (pair "" o single)
9.41 - val full_space =
9.42 - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
9.43 - fun add_facts global foldx facts =
9.44 - foldx (fn (name0, ths) =>
9.45 - if not exporter andalso name0 <> "" andalso
9.46 - forall (not o member Thm.eq_thm_prop add_ths) ths andalso
9.47 - (Facts.is_concealed facts name0 orelse
9.48 - (not (Config.get ctxt ignore_no_atp) andalso
9.49 - is_package_def name0) orelse
9.50 - exists (fn s => String.isSuffix s name0)
9.51 - (multi_base_blacklist ctxt ho_atp)) then
9.52 - I
9.53 - else
9.54 - let
9.55 - val multi = length ths > 1
9.56 - val backquote_thm =
9.57 - backquote o hackish_string_for_term ctxt o close_form o prop_of
9.58 - fun check_thms a =
9.59 - case try (Proof_Context.get_thms ctxt) a of
9.60 - NONE => false
9.61 - | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
9.62 - in
9.63 - pair 1
9.64 - #> fold (fn th => fn (j, (multis, unis)) =>
9.65 - (j + 1,
9.66 - if not (member Thm.eq_thm_prop add_ths th) andalso
9.67 - is_theorem_bad_for_atps ho_atp exporter th then
9.68 - (multis, unis)
9.69 - else
9.70 - let
9.71 - val new =
9.72 - (((fn () =>
9.73 - if name0 = "" then
9.74 - th |> backquote_thm
9.75 - else
9.76 - [Facts.extern ctxt facts name0,
9.77 - Name_Space.extern ctxt full_space name0,
9.78 - name0]
9.79 - |> find_first check_thms
9.80 - |> (fn SOME name =>
9.81 - make_name reserved multi j name
9.82 - | NONE => "")),
9.83 - stature_of_thm global assms chained_ths
9.84 - css_table name0 th), th)
9.85 - in
9.86 - if multi then (new :: multis, unis)
9.87 - else (multis, new :: unis)
9.88 - end)) ths
9.89 - #> snd
9.90 - end)
9.91 - in
9.92 - (* The single-name theorems go after the multiple-name ones, so that single
9.93 - names are preferred when both are available. *)
9.94 - ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
9.95 - |> add_facts true Facts.fold_static global_facts global_facts
9.96 - |> op @
9.97 - end
9.98 -
9.99 fun clasimpset_rule_table_of ctxt =
9.100 let
9.101 val thy = Proof_Context.theory_of ctxt
9.102 @@ -416,6 +346,84 @@
9.103 fun maybe_filter_no_atps ctxt =
9.104 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
9.105
9.106 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
9.107 + let
9.108 + val thy = Proof_Context.theory_of ctxt
9.109 + val global_facts = Global_Theory.facts_of thy
9.110 + val local_facts = Proof_Context.facts_of ctxt
9.111 + val named_locals = local_facts |> Facts.dest_static []
9.112 + val assms = Assumption.all_assms_of ctxt
9.113 + fun is_good_unnamed_local th =
9.114 + not (Thm.has_name_hint th) andalso
9.115 + forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
9.116 + val unnamed_locals =
9.117 + union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
9.118 + |> filter is_good_unnamed_local |> map (pair "" o single)
9.119 + val full_space =
9.120 + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
9.121 + fun add_facts global foldx facts =
9.122 + foldx (fn (name0, ths) =>
9.123 + if not exporter andalso name0 <> "" andalso
9.124 + forall (not o member Thm.eq_thm_prop add_ths) ths andalso
9.125 + (Facts.is_concealed facts name0 orelse
9.126 + (not (Config.get ctxt ignore_no_atp) andalso
9.127 + is_package_def name0) orelse
9.128 + exists (fn s => String.isSuffix s name0)
9.129 + (multi_base_blacklist ctxt ho_atp)) then
9.130 + I
9.131 + else
9.132 + let
9.133 + val multi = length ths > 1
9.134 + val backquote_thm =
9.135 + backquote o hackish_string_for_term ctxt o close_form o prop_of
9.136 + fun check_thms a =
9.137 + case try (Proof_Context.get_thms ctxt) a of
9.138 + NONE => false
9.139 + | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
9.140 + in
9.141 + pair 1
9.142 + #> fold (fn th => fn (j, (multis, unis)) =>
9.143 + (j + 1,
9.144 + if not (member Thm.eq_thm_prop add_ths th) andalso
9.145 + is_theorem_bad_for_atps ho_atp exporter th then
9.146 + (multis, unis)
9.147 + else
9.148 + let
9.149 + val new =
9.150 + (((fn () =>
9.151 + if name0 = "" then
9.152 + th |> backquote_thm
9.153 + else
9.154 + [Facts.extern ctxt facts name0,
9.155 + Name_Space.extern ctxt full_space name0,
9.156 + name0]
9.157 + |> find_first check_thms
9.158 + |> (fn SOME name =>
9.159 + make_name reserved multi j name
9.160 + | NONE => "")),
9.161 + stature_of_thm global assms chained_ths
9.162 + css_table name0 th), th)
9.163 + in
9.164 + if multi then (new :: multis, unis)
9.165 + else (multis, new :: unis)
9.166 + end)) ths
9.167 + #> snd
9.168 + end)
9.169 + in
9.170 + (* The single-name theorems go after the multiple-name ones, so that single
9.171 + names are preferred when both are available. *)
9.172 + ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
9.173 + |> add_facts true Facts.fold_static global_facts global_facts
9.174 + |> op @
9.175 + end
9.176 +
9.177 +fun all_facts_of thy =
9.178 + let val ctxt = Proof_Context.init_global thy in
9.179 + all_facts ctxt false Symtab.empty true [] []
9.180 + (clasimpset_rule_table_of ctxt)
9.181 + |> rev (* try to restore the original order of facts, for MaSh *)
9.182 + end
9.183 +
9.184 fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
9.185 chained_ths hyp_ts concl_t =
9.186 if only andalso null add then
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200
10.3 @@ -6,6 +6,35 @@
10.4
10.5 signature SLEDGEHAMMER_FILTER_MASH =
10.6 sig
10.7 + type status = ATP_Problem_Generate.status
10.8 + type stature = ATP_Problem_Generate.stature
10.9 + type params = Sledgehammer_Provers.params
10.10 + type prover_result = Sledgehammer_Provers.prover_result
10.11 +
10.12 + val fact_name_of : string -> string
10.13 + val all_non_tautological_facts_of :
10.14 + theory -> (((unit -> string) * stature) * thm) list
10.15 + val theory_ord : theory * theory -> order
10.16 + val thm_ord : thm * thm -> order
10.17 + val thms_by_thy : ('a * thm) list -> (string * thm list) list
10.18 + val has_thy : theory -> thm -> bool
10.19 + val parent_thms : (string * thm list) list -> theory -> string list
10.20 + val features_of : theory -> status * thm -> string list
10.21 + val isabelle_dependencies_of : string list -> thm -> string list
10.22 + val goal_of_thm : theory -> thm -> thm
10.23 + val iter_facts :
10.24 + Proof.context -> params -> int -> thm
10.25 + -> (((unit -> string) * stature) * thm) list
10.26 + -> ((string * stature) * thm) list
10.27 + val run_prover :
10.28 + Proof.context -> params -> ((string * stature) * thm) list -> thm
10.29 + -> prover_result
10.30 + val generate_accessibility : theory -> bool -> string -> unit
10.31 + val generate_features : theory -> bool -> string -> unit
10.32 + val generate_isa_dependencies : theory -> bool -> string -> unit
10.33 + val generate_atp_dependencies :
10.34 + Proof.context -> params -> theory -> bool -> string -> unit
10.35 +
10.36 val reset : unit -> unit
10.37 val can_suggest : unit -> bool
10.38 val can_learn_thy : theory -> bool
10.39 @@ -16,6 +45,16 @@
10.40 structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
10.41 struct
10.42
10.43 +open ATP_Util
10.44 +open ATP_Problem_Generate
10.45 +open Sledgehammer_Util
10.46 +open Sledgehammer_Fact
10.47 +open Sledgehammer_Filter_Iter
10.48 +open Sledgehammer_Provers
10.49 +
10.50 +
10.51 +(*** Low-level communication with MaSh ***)
10.52 +
10.53 fun mash_reset () =
10.54 tracing "MaSh RESET"
10.55
10.56 @@ -30,6 +69,311 @@
10.57 tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
10.58 space_implode " " feats)
10.59
10.60 +
10.61 +(*** Isabelle helpers ***)
10.62 +
10.63 +val fact_name_of = prefix fact_prefix o ascii_of
10.64 +
10.65 +fun escape_meta_char c =
10.66 + if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
10.67 + c = #")" orelse c = #"," then
10.68 + String.str c
10.69 + else
10.70 + (* fixed width, in case more digits follow *)
10.71 + "\\" ^ stringN_of_int 3 (Char.ord c)
10.72 +
10.73 +val escape_meta = String.translate escape_meta_char
10.74 +
10.75 +val thy_prefix = "y_"
10.76 +
10.77 +val fact_name_of = escape_meta
10.78 +val thy_name_of = prefix thy_prefix o escape_meta
10.79 +val const_name_of = prefix const_prefix o escape_meta
10.80 +val type_name_of = prefix type_const_prefix o escape_meta
10.81 +val class_name_of = prefix class_prefix o escape_meta
10.82 +
10.83 +val thy_name_of_thm = theory_of_thm #> Context.theory_name
10.84 +
10.85 +local
10.86 +
10.87 +fun has_bool @{typ bool} = true
10.88 + | has_bool (Type (_, Ts)) = exists has_bool Ts
10.89 + | has_bool _ = false
10.90 +
10.91 +fun has_fun (Type (@{type_name fun}, _)) = true
10.92 + | has_fun (Type (_, Ts)) = exists has_fun Ts
10.93 + | has_fun _ = false
10.94 +
10.95 +val is_conn = member (op =)
10.96 + [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
10.97 + @{const_name HOL.implies}, @{const_name Not},
10.98 + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
10.99 + @{const_name HOL.eq}]
10.100 +
10.101 +val has_bool_arg_const =
10.102 + exists_Const (fn (c, T) =>
10.103 + not (is_conn c) andalso exists has_bool (binder_types T))
10.104 +
10.105 +fun higher_inst_const thy (c, T) =
10.106 + case binder_types T of
10.107 + [] => false
10.108 + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
10.109 +
10.110 +val binders = [@{const_name All}, @{const_name Ex}]
10.111 +
10.112 +in
10.113 +
10.114 +fun is_fo_term thy t =
10.115 + let
10.116 + val t =
10.117 + t |> Envir.beta_eta_contract
10.118 + |> transform_elim_prop
10.119 + |> Object_Logic.atomize_term thy
10.120 + in
10.121 + Term.is_first_order binders t andalso
10.122 + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
10.123 + | _ => false) t orelse
10.124 + has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
10.125 + end
10.126 +
10.127 +end
10.128 +
10.129 +fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
10.130 + let
10.131 + val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
10.132 + val bad_consts = atp_widely_irrelevant_consts
10.133 + fun do_add_type (Type (s, Ts)) =
10.134 + (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
10.135 + #> fold do_add_type Ts
10.136 + | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
10.137 + | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
10.138 + fun add_type T = type_max_depth >= 0 ? do_add_type T
10.139 + fun mk_app s args =
10.140 + if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
10.141 + else s
10.142 + fun patternify ~1 _ = ""
10.143 + | patternify depth t =
10.144 + case strip_comb t of
10.145 + (Const (s, _), args) =>
10.146 + mk_app (const_name_of s) (map (patternify (depth - 1)) args)
10.147 + | _ => ""
10.148 + fun add_term_patterns ~1 _ = I
10.149 + | add_term_patterns depth t =
10.150 + insert (op =) (patternify depth t)
10.151 + #> add_term_patterns (depth - 1) t
10.152 + val add_term = add_term_patterns term_max_depth
10.153 + fun add_patterns t =
10.154 + let val (head, args) = strip_comb t in
10.155 + (case head of
10.156 + Const (s, T) =>
10.157 + not (member (op =) bad_consts s) ? (add_term t #> add_type T)
10.158 + | Free (_, T) => add_type T
10.159 + | Var (_, T) => add_type T
10.160 + | Abs (_, T, body) => add_type T #> add_patterns body
10.161 + | _ => I)
10.162 + #> fold add_patterns args
10.163 + end
10.164 + in [] |> add_patterns t |> sort string_ord end
10.165 +
10.166 +fun is_likely_tautology th =
10.167 + null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
10.168 + not (Thm.eq_thm_prop (@{thm ext}, th))
10.169 +
10.170 +fun is_too_meta thy th =
10.171 + fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
10.172 +
10.173 +fun all_non_tautological_facts_of thy =
10.174 + all_facts_of thy
10.175 + |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
10.176 +
10.177 +fun theory_ord p =
10.178 + if Theory.eq_thy p then EQUAL
10.179 + else if Theory.subthy p then LESS
10.180 + else if Theory.subthy (swap p) then GREATER
10.181 + else EQUAL
10.182 +
10.183 +val thm_ord = theory_ord o pairself theory_of_thm
10.184 +
10.185 +fun thms_by_thy ths =
10.186 + ths |> map (snd #> `thy_name_of_thm)
10.187 + |> AList.group (op =)
10.188 + |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
10.189 + o hd o snd))
10.190 + |> map (apsnd (sort thm_ord))
10.191 +
10.192 +fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
10.193 +
10.194 +fun parent_thms thy_ths thy =
10.195 + Theory.parents_of thy
10.196 + |> map Context.theory_name
10.197 + |> map_filter (AList.lookup (op =) thy_ths)
10.198 + |> map List.last
10.199 + |> map (fact_name_of o Thm.get_name_hint)
10.200 +
10.201 +fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
10.202 +
10.203 +val max_depth = 1
10.204 +
10.205 +(* TODO: Generate type classes for types? *)
10.206 +fun features_of thy (status, th) =
10.207 + let val t = Thm.prop_of th in
10.208 + thy_name_of (thy_name_of_thm th) ::
10.209 + interesting_terms_types_and_classes max_depth max_depth t
10.210 + |> not (has_no_lambdas t) ? cons "lambdas"
10.211 + |> exists_Const is_exists t ? cons "skolems"
10.212 + |> not (is_fo_term thy t) ? cons "ho"
10.213 + |> (case status of
10.214 + General => I
10.215 + | Induction => cons "induction"
10.216 + | Intro => cons "intro"
10.217 + | Inductive => cons "inductive"
10.218 + | Elim => cons "elim"
10.219 + | Simp => cons "simp"
10.220 + | Def => cons "def")
10.221 + end
10.222 +
10.223 +fun isabelle_dependencies_of all_facts =
10.224 + thms_in_proof (SOME all_facts)
10.225 + #> map fact_name_of #> sort string_ord
10.226 +
10.227 +val freezeT = Type.legacy_freeze_type
10.228 +
10.229 +fun freeze (t $ u) = freeze t $ freeze u
10.230 + | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
10.231 + | freeze (Var ((s, _), T)) = Free (s, freezeT T)
10.232 + | freeze (Const (s, T)) = Const (s, freezeT T)
10.233 + | freeze (Free (s, T)) = Free (s, freezeT T)
10.234 + | freeze t = t
10.235 +
10.236 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
10.237 +
10.238 +fun iter_facts ctxt ({provers, relevance_thresholds, ...} : params) max_relevant
10.239 + goal =
10.240 + let
10.241 + val prover_name = hd provers
10.242 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
10.243 + val is_built_in_const =
10.244 + Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
10.245 + val relevance_fudge =
10.246 + Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
10.247 + val relevance_override = {add = [], del = [], only = false}
10.248 + in
10.249 + iterative_relevant_facts ctxt relevance_thresholds max_relevant
10.250 + is_built_in_const relevance_fudge
10.251 + relevance_override [] hyp_ts concl_t
10.252 + end
10.253 +
10.254 +fun run_prover ctxt (params as {provers, ...}) facts goal =
10.255 + let
10.256 + val problem =
10.257 + {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
10.258 + facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
10.259 + val prover =
10.260 + Sledgehammer_Minimize.get_minimizing_prover ctxt
10.261 + Sledgehammer_Provers.Normal (hd provers)
10.262 + in prover params (K (K (K ""))) problem end
10.263 +
10.264 +fun generate_accessibility thy include_thy file_name =
10.265 + let
10.266 + val path = file_name |> Path.explode
10.267 + val _ = File.write path ""
10.268 + fun do_thm th prevs =
10.269 + let
10.270 + val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
10.271 + val _ = File.append path s
10.272 + in [th] end
10.273 + val thy_ths =
10.274 + all_non_tautological_facts_of thy
10.275 + |> not include_thy ? filter_out (has_thy thy o snd)
10.276 + |> thms_by_thy
10.277 + fun do_thy ths =
10.278 + let
10.279 + val thy = theory_of_thm (hd ths)
10.280 + val parents = parent_thms thy_ths thy
10.281 + val ths = ths |> map (fact_name_of o Thm.get_name_hint)
10.282 + in fold do_thm ths parents; () end
10.283 + in List.app (do_thy o snd) thy_ths end
10.284 +
10.285 +fun generate_features thy include_thy file_name =
10.286 + let
10.287 + val path = file_name |> Path.explode
10.288 + val _ = File.write path ""
10.289 + val facts =
10.290 + all_non_tautological_facts_of thy
10.291 + |> not include_thy ? filter_out (has_thy thy o snd)
10.292 + fun do_fact ((_, (_, status)), th) =
10.293 + let
10.294 + val name = Thm.get_name_hint th
10.295 + val feats = features_of thy (status, th)
10.296 + val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
10.297 + in File.append path s end
10.298 + in List.app do_fact facts end
10.299 +
10.300 +fun generate_isa_dependencies thy include_thy file_name =
10.301 + let
10.302 + val path = file_name |> Path.explode
10.303 + val _ = File.write path ""
10.304 + val ths =
10.305 + all_non_tautological_facts_of thy
10.306 + |> not include_thy ? filter_out (has_thy thy o snd)
10.307 + |> map snd
10.308 + val all_names = ths |> map Thm.get_name_hint
10.309 + fun do_thm th =
10.310 + let
10.311 + val name = Thm.get_name_hint th
10.312 + val deps = isabelle_dependencies_of all_names th
10.313 + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
10.314 + in File.append path s end
10.315 + in List.app do_thm ths end
10.316 +
10.317 +fun generate_atp_dependencies ctxt (params as {max_relevant, ...}) thy
10.318 + include_thy file_name =
10.319 + let
10.320 + val path = file_name |> Path.explode
10.321 + val _ = File.write path ""
10.322 + val facts =
10.323 + all_non_tautological_facts_of thy
10.324 + |> not include_thy ? filter_out (has_thy thy o snd)
10.325 + val ths = facts |> map snd
10.326 + val all_names = ths |> map Thm.get_name_hint
10.327 + fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
10.328 + fun add_isa_dep facts dep accum =
10.329 + if exists (is_dep dep) accum then
10.330 + accum
10.331 + else case find_first (is_dep dep) facts of
10.332 + SOME ((name, status), th) => accum @ [((name (), status), th)]
10.333 + | NONE => accum (* shouldn't happen *)
10.334 + fun fix_name ((_, stature), th) =
10.335 + ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
10.336 + fun do_thm th =
10.337 + let
10.338 + val name = Thm.get_name_hint th
10.339 + val goal = goal_of_thm thy th
10.340 + val deps =
10.341 + case isabelle_dependencies_of all_names th of
10.342 + [] => []
10.343 + | isa_dep as [_] => isa_dep (* can hardly beat that *)
10.344 + | isa_deps =>
10.345 + let
10.346 + val facts =
10.347 + facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
10.348 + val facts =
10.349 + facts |> iter_facts ctxt params (the max_relevant) goal
10.350 + |> fold (add_isa_dep facts) isa_deps
10.351 + |> map fix_name
10.352 + in
10.353 + case run_prover ctxt params facts goal of
10.354 + {outcome = NONE, used_facts, ...} =>
10.355 + used_facts |> map fst |> sort string_ord
10.356 + | _ => isa_deps
10.357 + end
10.358 + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
10.359 + in File.append path s end
10.360 + in List.app do_thm ths end
10.361 +
10.362 +
10.363 +(*** High-level communication with MaSh ***)
10.364 +
10.365 fun reset () =
10.366 ()
10.367
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
11.3 @@ -14,6 +14,7 @@
11.4 val subgoal_count : Proof.state -> int
11.5 val normalize_chained_theorems : thm list -> thm list
11.6 val reserved_isar_keyword_table : unit -> unit Symtab.table
11.7 + val thms_in_proof : string list option -> thm -> string list
11.8 end;
11.9
11.10 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
11.11 @@ -60,4 +61,36 @@
11.12 Keyword.dest () |-> union (op =)
11.13 |> map (rpair ()) |> Symtab.make
11.14
11.15 +(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
11.16 + fixes that seem to be missing over there; or maybe the two code portions are
11.17 + not doing the same? *)
11.18 +fun fold_body_thms thm_name f =
11.19 + let
11.20 + fun app n (PBody {thms, ...}) =
11.21 + thms |> fold (fn (_, (name, prop, body)) => fn x =>
11.22 + let
11.23 + val body' = Future.join body
11.24 + val n' =
11.25 + n + (if name = "" orelse
11.26 + (* uncommon case where the proved theorem occurs twice
11.27 + (e.g., "Transitive_Closure.trancl_into_trancl") *)
11.28 + (n = 1 andalso name = thm_name) then
11.29 + 0
11.30 + else
11.31 + 1)
11.32 + val x' = x |> n' <= 1 ? app n' body'
11.33 + in (x' |> n = 1 ? f (name, prop, body')) end)
11.34 + in fold (app 0) end
11.35 +
11.36 +fun thms_in_proof all_names th =
11.37 + let
11.38 + val is_name_ok =
11.39 + case all_names of
11.40 + SOME names => member (op =) names
11.41 + | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
11.42 + fun collect (s, _, _) = is_name_ok s ? insert (op =) s
11.43 + val names =
11.44 + [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
11.45 + in names end
11.46 +
11.47 end;