1.1 --- a/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 17:01:48 2014 +0200
1.2 +++ b/src/Doc/Sledgehammer/document/root.tex Tue Jul 01 17:06:54 2014 +0200
1.3 @@ -1059,22 +1059,26 @@
1.4 The MaSh machine learner. Three learning engines are provided:
1.5
1.6 \begin{enum}
1.7 -\item[\labelitemi] \textbf{\textit{nb}} (also called \textbf{\textit{sml}}
1.8 -and \textbf{\textit{yes}}) is a Standard ML implementation of naive Bayes.
1.9 +\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
1.10
1.11 -\item[\labelitemi] \textbf{\textit{knn}} is a Standard ML implementation of
1.12 -$k$-nearest neighbors.
1.13 +\item[\labelitemi] \textbf{\textit{knn}} is an implementation of $k$-nearest
1.14 +neighbors.
1.15 +
1.16 +\item[\labelitemi] \textbf{\textit{nb\_knn}} (also called \textbf{\textit{yes}}
1.17 +and \textbf{\textit{sml}}) is a combination of naive Bayes and $k$-nearest
1.18 +neighbors.
1.19 \end{enum}
1.20
1.21 In addition, the special value \textit{none} is used to disable machine learning by
1.22 default (cf.\ \textit{smart} below).
1.23
1.24 -The engine can be selected by setting \texttt{MASH} to the name of the desired
1.25 -engine---either in the environment in which Isabelle is launched, in your
1.26 -\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``MaSh'' option
1.27 -under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
1.28 -Persistent data for both engines is stored in the directory
1.29 -\texttt{\$ISABELLE\_HOME\_USER/mash}.
1.30 +The default engine is \textit{nb\_knn}. The engine can be selected by setting
1.31 +\texttt{MASH} to the name of the desired engine---either in the environment in
1.32 +which Isabelle is launched, in your
1.33 +\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
1.34 +file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
1.35 +General'' in Isabelle/jEdit. Persistent data for both engines is stored in the
1.36 +directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
1.37
1.38 \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
1.39 rankings from MePo and MaSh.
2.1 --- a/src/HOL/TPTP/MaSh_Eval.thy Tue Jul 01 17:01:48 2014 +0200
2.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy Tue Jul 01 17:06:54 2014 +0200
2.3 @@ -11,11 +11,8 @@
2.4 ML_file "mash_eval.ML"
2.5
2.6 sledgehammer_params
2.7 - [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
2.8 - lam_trans = lifting, timeout = 15, dont_preplay, minimize]
2.9 -
2.10 -declare [[sledgehammer_fact_duplicates = true]]
2.11 -declare [[sledgehammer_instantiate_inducts = false]]
2.12 + [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
2.13 + lam_trans = combs, timeout = 30, dont_preplay, minimize]
2.14
2.15 ML {*
2.16 Multithreading.max_threads_value ()
2.17 @@ -43,15 +40,13 @@
2.18
2.19 ML {*
2.20 if do_it then
2.21 - evaluate_mash_suggestions @{context} params range
2.22 - [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
2.23 - (SOME prob_dir)
2.24 - (prefix ^ "mepo_suggestions")
2.25 - (prefix ^ "mash_suggestions")
2.26 - (prefix ^ "mash_prover_suggestions")
2.27 - (prefix ^ "mesh_suggestions")
2.28 - (prefix ^ "mesh_prover_suggestions")
2.29 - (prefix ^ "mash_eval")
2.30 + evaluate_mash_suggestions @{context} params range (SOME prob_dir)
2.31 + [prefix ^ "mepo_suggestions",
2.32 + prefix ^ "mash_suggestions",
2.33 + prefix ^ "mash_prover_suggestions",
2.34 + prefix ^ "mesh_suggestions",
2.35 + prefix ^ "mesh_prover_suggestions"]
2.36 + (prefix ^ "mash_eval")
2.37 else
2.38 ()
2.39 *}
3.1 --- a/src/HOL/TPTP/MaSh_Export.thy Tue Jul 01 17:01:48 2014 +0200
3.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Tue Jul 01 17:06:54 2014 +0200
3.3 @@ -46,32 +46,74 @@
3.4 ()
3.5 *}
3.6
3.7 -ML {* Options.put_default @{system_option MaSh} "nb" *}
3.8 -
3.9 ML {*
3.10 if do_it then
3.11 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
3.12 + generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions
3.13 (prefix ^ "mash_nb_suggestions")
3.14 else
3.15 ()
3.16 *}
3.17
3.18 -ML {* Options.put_default @{system_option MaSh} "knn" *}
3.19 -
3.20 ML {*
3.21 if do_it then
3.22 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
3.23 + generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions
3.24 (prefix ^ "mash_knn_suggestions")
3.25 else
3.26 ()
3.27 *}
3.28
3.29 -ML {* Options.put_default @{system_option MaSh} "py" *}
3.30 +ML {*
3.31 +if do_it then
3.32 + generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
3.33 + (prefix ^ "mepo_suggestions")
3.34 +else
3.35 + ()
3.36 +*}
3.37
3.38 ML {*
3.39 if do_it then
3.40 - generate_mash_suggestions @{context} params (range, step) thys max_suggestions
3.41 - (prefix ^ "mash_py_suggestions")
3.42 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions")
3.43 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions")
3.44 +else
3.45 + ()
3.46 +*}
3.47 +
3.48 +ML {*
3.49 +if do_it then
3.50 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions")
3.51 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions")
3.52 +else
3.53 + ()
3.54 +*}
3.55 +
3.56 +ML {*
3.57 +if do_it then
3.58 + generate_prover_dependencies @{context} params range thys
3.59 + (prefix ^ "mash_nb_prover_dependencies")
3.60 +else
3.61 + ()
3.62 +*}
3.63 +
3.64 +ML {*
3.65 +if do_it then
3.66 + generate_prover_dependencies @{context} params range thys
3.67 + (prefix ^ "mash_knn_prover_dependencies")
3.68 +else
3.69 + ()
3.70 +*}
3.71 +
3.72 +ML {*
3.73 +if do_it then
3.74 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions")
3.75 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions")
3.76 +else
3.77 + ()
3.78 +*}
3.79 +
3.80 +ML {*
3.81 +if do_it then
3.82 + generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions")
3.83 + (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions")
3.84 else
3.85 ()
3.86 *}
3.87 @@ -107,41 +149,10 @@
3.88
3.89 ML {*
3.90 if do_it then
3.91 - generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
3.92 - (prefix ^ "mepo_suggestions")
3.93 -else
3.94 - ()
3.95 -*}
3.96 -
3.97 -ML {*
3.98 -if do_it then
3.99 - generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
3.100 - (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
3.101 -else
3.102 - ()
3.103 -*}
3.104 -
3.105 -ML {*
3.106 -if do_it then
3.107 - generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies")
3.108 -else
3.109 - ()
3.110 -*}
3.111 -
3.112 -ML {*
3.113 -if do_it then
3.114 generate_prover_commands @{context} params (range, step) thys max_suggestions
3.115 (prefix ^ "mash_prover_commands")
3.116 else
3.117 ()
3.118 *}
3.119
3.120 -ML {*
3.121 -if do_it then
3.122 - generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
3.123 - (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
3.124 -else
3.125 - ()
3.126 -*}
3.127 -
3.128 end
4.1 --- a/src/HOL/TPTP/mash_eval.ML Tue Jul 01 17:01:48 2014 +0200
4.2 +++ b/src/HOL/TPTP/mash_eval.ML Tue Jul 01 17:06:54 2014 +0200
4.3 @@ -9,14 +9,8 @@
4.4 sig
4.5 type params = Sledgehammer_Prover.params
4.6
4.7 - val MePoN : string
4.8 - val MaSh_IsarN : string
4.9 - val MaSh_ProverN : string
4.10 - val MeSh_IsarN : string
4.11 - val MeSh_ProverN : string
4.12 - val IsarN : string
4.13 - val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string list ->
4.14 - string option -> string -> string -> string -> string -> string -> string -> unit
4.15 + val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string option ->
4.16 + string list -> string -> unit
4.17 end;
4.18
4.19 structure MaSh_Eval : MASH_EVAL =
4.20 @@ -33,15 +27,7 @@
4.21
4.22 val prefix = Library.prefix
4.23
4.24 -val MaSh_IsarN = MaShN ^ "-Isar"
4.25 -val MaSh_ProverN = MaShN ^ "-Prover"
4.26 -val MeSh_IsarN = MeShN ^ "-Isar"
4.27 -val MeSh_ProverN = MeShN ^ "-Prover"
4.28 -val IsarN = "Isar"
4.29 -
4.30 -fun evaluate_mash_suggestions ctxt params range methods prob_dir_name mepo_file_name
4.31 - mash_isar_file_name mash_prover_file_name mesh_isar_file_name mesh_prover_file_name
4.32 - report_file_name =
4.33 +fun evaluate_mash_suggestions ctxt params range prob_dir_name file_names report_file_name =
4.34 let
4.35 val thy = Proof_Context.theory_of ctxt
4.36 val zeros = [0, 0, 0, 0, 0, 0]
4.37 @@ -53,20 +39,19 @@
4.38 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
4.39 val prover = hd provers
4.40 val max_suggs = generous_max_suggestions (the max_facts)
4.41 +
4.42 + val method_of_file_name =
4.43 + perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
4.44 +
4.45 + val methods = "isar" :: map method_of_file_name file_names
4.46 val lines_of = Path.explode #> try File.read_lines #> these
4.47 - val file_names =
4.48 - [mepo_file_name, mash_isar_file_name, mash_prover_file_name,
4.49 - mesh_isar_file_name, mesh_prover_file_name]
4.50 - val lines as [mepo_lines, mash_isar_lines, mash_prover_lines,
4.51 - mesh_isar_lines, mesh_prover_lines] =
4.52 - map lines_of file_names
4.53 - val num_lines = fold (Integer.max o length) lines 0
4.54 + val liness0 = map lines_of file_names
4.55 + val num_lines = fold (Integer.max o length) liness0 0
4.56
4.57 fun pad lines = lines @ replicate (num_lines - length lines) ""
4.58
4.59 - val lines =
4.60 - pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
4.61 - pad mesh_isar_lines ~~ pad mesh_prover_lines
4.62 + val liness = map pad liness0
4.63 +
4.64 val css = clasimpset_rule_table_of ctxt
4.65 val facts = all_facts ctxt true false Symtab.empty [] [] css
4.66 val name_tabs = build_name_tables nickname_of_thm facts
4.67 @@ -95,19 +80,12 @@
4.68 |> space_implode " "))
4.69 end
4.70
4.71 - fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), mesh_isar_line),
4.72 - mesh_prover_line)) =
4.73 + fun solve_goal (j, lines) =
4.74 if in_range range j then
4.75 let
4.76 val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
4.77 - val (name1, mepo_suggs) = get_suggs mepo_line
4.78 - val (name2, mash_isar_suggs) = get_suggs mash_isar_line
4.79 - val (name3, mash_prover_suggs) = get_suggs mash_prover_line
4.80 - val (name4, mesh_isar_suggs) = get_suggs mesh_isar_line
4.81 - val (name5, mesh_prover_suggs) = get_suggs mesh_prover_line
4.82 - val [name] =
4.83 - [name1, name2, name3, name4, name5]
4.84 - |> filter (curry (op <>) "") |> distinct (op =)
4.85 + val (names, suggss0) = split_list (map get_suggs lines)
4.86 + val [name] = names |> filter (curry (op <>) "") |> distinct (op =)
4.87 handle General.Match => error "Input files out of sync."
4.88 val th =
4.89 case find_first (fn (_, th) => nickname_of_thm th = name) facts of
4.90 @@ -116,6 +94,7 @@
4.91 val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
4.92 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
4.93 val isar_deps = these (isar_dependencies_of name_tabs th)
4.94 + val suggss = isar_deps :: suggss0
4.95 val facts = facts |> filter (fn (_, th') => thm_less (th', th))
4.96
4.97 (* adapted from "mirabelle_sledgehammer.ML" *)
4.98 @@ -130,7 +109,7 @@
4.99 | set_file_name _ NONE = I
4.100
4.101 fun prove method suggs =
4.102 - if not (member (op =) methods method) orelse (null facts andalso method <> IsarN) then
4.103 + if null facts then
4.104 (str_of_method method ^ "Skipped", 0)
4.105 else
4.106 let
4.107 @@ -151,14 +130,7 @@
4.108 (str_of_result method facts res, ok)
4.109 end
4.110
4.111 - val ress =
4.112 - [fn () => prove MePoN mepo_suggs,
4.113 - fn () => prove MaSh_IsarN mash_isar_suggs,
4.114 - fn () => prove MaSh_ProverN mash_prover_suggs,
4.115 - fn () => prove MeSh_IsarN mesh_isar_suggs,
4.116 - fn () => prove MeSh_ProverN mesh_prover_suggs,
4.117 - fn () => prove IsarN isar_deps]
4.118 - |> (* Par_List. *) map (fn f => f ())
4.119 + val ress = map2 prove methods suggss
4.120 in
4.121 "Goal " ^ string_of_int j ^ ": " ^ name :: map fst ress
4.122 |> cat_lines |> print;
4.123 @@ -167,10 +139,6 @@
4.124 else
4.125 zeros
4.126
4.127 - fun total_of method ok n =
4.128 - str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
4.129 - (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
4.130 -
4.131 val inst_inducts = Config.get ctxt instantiate_inducts
4.132 val options =
4.133 ["prover = " ^ prover,
4.134 @@ -182,18 +150,17 @@
4.135 "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
4.136 val _ = print " * * *";
4.137 val _ = print ("Options: " ^ commas options);
4.138 - val oks = Par_List.map solve_goal (tag_list 1 lines)
4.139 + val oks = Par_List.map solve_goal (tag_list 1 liness)
4.140 val n = length oks
4.141 - val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, isar_ok] =
4.142 - if n = 0 then zeros else map Integer.sum (map_transpose I oks)
4.143 +
4.144 + fun total_of method ok =
4.145 + str_of_method method ^ string_of_int ok ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1))
4.146 + (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
4.147 +
4.148 + val oks' = if n = 0 then zeros else map Integer.sum (map_transpose I oks)
4.149 in
4.150 - ["Successes (of " ^ string_of_int n ^ " goals)",
4.151 - total_of MePoN mepo_ok n,
4.152 - total_of MaSh_IsarN mash_isar_ok n,
4.153 - total_of MaSh_ProverN mash_prover_ok n,
4.154 - total_of MeSh_IsarN mesh_isar_ok n,
4.155 - total_of MeSh_ProverN mesh_prover_ok n,
4.156 - total_of IsarN isar_ok n]
4.157 + "Successes (of " ^ string_of_int n ^ " goals)" ::
4.158 + map2 total_of methods oks'
4.159 |> cat_lines |> print
4.160 end
4.161
5.1 --- a/src/HOL/TPTP/mash_export.ML Tue Jul 01 17:01:48 2014 +0200
5.2 +++ b/src/HOL/TPTP/mash_export.ML Tue Jul 01 17:06:54 2014 +0200
5.3 @@ -24,7 +24,7 @@
5.4 theory list -> int -> string -> unit
5.5 val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
5.6 theory list -> int -> string -> unit
5.7 - val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int ->
5.8 + val generate_mash_suggestions : string -> Proof.context -> params -> (int * int option) * int ->
5.9 theory list -> int -> string -> unit
5.10 val generate_mesh_suggestions : int -> string -> string -> string -> unit
5.11 end;
5.12 @@ -284,15 +284,16 @@
5.13 not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
5.14 #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
5.15
5.16 -fun generate_mash_suggestions ctxt params =
5.17 - (Sledgehammer_MaSh.mash_unlearn ();
5.18 +fun generate_mash_suggestions engine =
5.19 + (Options.put_default @{system_option MaSh} engine;
5.20 + Sledgehammer_MaSh.mash_unlearn ();
5.21 generate_mepo_or_mash_suggestions
5.22 (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
5.23 fn concl_t =>
5.24 tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
5.25 Sledgehammer_Util.one_year)
5.26 #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
5.27 - #> fst) ctxt params)
5.28 + #> fst))
5.29
5.30 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
5.31 let
6.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 01 17:01:48 2014 +0200
6.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 01 17:06:54 2014 +0200
6.3 @@ -749,11 +749,9 @@
6.4
6.5 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
6.6 fun conceal_bounds Ts t =
6.7 - subst_bounds (map (Free o apfst concealed_bound_name)
6.8 - (0 upto length Ts - 1 ~~ Ts), t)
6.9 + subst_bounds (map_index (Free o apfst concealed_bound_name) Ts, t)
6.10 fun reveal_bounds Ts =
6.11 - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
6.12 - (0 upto length Ts - 1 ~~ Ts))
6.13 + subst_atomic (map_index (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) Ts)
6.14
6.15 fun do_introduce_combinators ctxt Ts t =
6.16 let val thy = Proof_Context.theory_of ctxt in
6.17 @@ -1327,7 +1325,7 @@
6.18 if forall null footprint then
6.19 []
6.20 else
6.21 - 0 upto length footprint - 1 ~~ footprint
6.22 + map_index I footprint
6.23 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
6.24 |> cover []
6.25 end
6.26 @@ -1878,7 +1876,7 @@
6.27 val conjs =
6.28 map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
6.29 |> map (apsnd freeze_term)
6.30 - |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
6.31 + |> map_index (uncurry (pair o rpair (Local, General) o string_of_int))
6.32 val ((conjs, facts), lam_facts) =
6.33 (conjs, facts)
6.34 |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
6.35 @@ -1930,7 +1928,7 @@
6.36 val cover = type_arg_cover thy pos s ary
6.37 in
6.38 exists (fn (j, tm) => tm = var andalso member (op =) cover j)
6.39 - (0 upto ary - 1 ~~ tms) orelse
6.40 + (0 upto ary - 1 ~~ tms) orelse
6.41 exists is_undercover tms
6.42 end
6.43 | is_undercover _ = true
6.44 @@ -1984,7 +1982,7 @@
6.45 val ary = length args
6.46 fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
6.47 in
6.48 - map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
6.49 + map_index (uncurry (term o arg_site)) args
6.50 |> mk_aterm type_enc name T_args
6.51 end
6.52 | IVar (name, _) =>
6.53 @@ -2102,7 +2100,7 @@
6.54 if is_type_enc_polymorphic type_enc then
6.55 let
6.56 val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
6.57 - fun line j (cl, T) =
6.58 + fun line (j, (cl, T)) =
6.59 if type_classes then
6.60 Class_Memb (class_memb_prefix ^ string_of_int j, [],
6.61 native_atp_type_of_typ type_enc false 0 T, `make_class cl)
6.62 @@ -2113,7 +2111,7 @@
6.63 fold (union (op =)) (map #atomic_types facts) []
6.64 |> class_membs_of_types type_enc add_sorts_on_tfree
6.65 in
6.66 - map2 line (0 upto length membs - 1) membs
6.67 + map_index line membs
6.68 end
6.69 else
6.70 []
6.71 @@ -2314,8 +2312,7 @@
6.72
6.73 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
6.74
6.75 -fun line_of_guards_sym_decl ctxt mono type_enc n s j
6.76 - (s', T_args, T, _, ary, in_conj) =
6.77 +fun line_of_guards_sym_decl ctxt mono type_enc n s j (s', T_args, T, _, ary, in_conj) =
6.78 let
6.79 val thy = Proof_Context.theory_of ctxt
6.80 val (role, maybe_negate) = honor_conj_sym_role in_conj
6.81 @@ -2328,7 +2325,7 @@
6.82 All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
6.83 | Undercover_Types =>
6.84 let val cover = type_arg_cover thy NONE s ary in
6.85 - map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts
6.86 + map_index (uncurry (fn j => if member (op =) cover j then SOME else K NONE)) arg_Ts
6.87 end
6.88 | _ => replicate ary NONE)
6.89 in
6.90 @@ -2372,7 +2369,7 @@
6.91 let
6.92 val cover = type_arg_cover thy NONE s ary
6.93 fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
6.94 - val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
6.95 + val bounds = map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts) bounds
6.96 in formula (cst bounds) end
6.97 else
6.98 formula (cst bounds)
6.99 @@ -2399,14 +2396,14 @@
6.100 val n = length decls
6.101 val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
6.102 in
6.103 - (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
6.104 + map_index (uncurry (line_of_guards_sym_decl ctxt mono type_enc n s)) decls
6.105 end
6.106 | Tags (_, level) =>
6.107 if is_type_level_uniform level then
6.108 []
6.109 else
6.110 let val n = length decls in
6.111 - (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
6.112 + maps (lines_of_tags_sym_decl ctxt mono type_enc n s) (0 upto n - 1 ~~ decls)
6.113 end)
6.114
6.115 fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
6.116 @@ -2603,6 +2600,7 @@
6.117 val thy = Proof_Context.theory_of ctxt
6.118 val type_enc = type_enc |> adjust_type_enc format
6.119 val completish = (mode = Sledgehammer_Completish)
6.120 +
6.121 (* Forcing explicit applications is expensive for polymorphic encodings,
6.122 because it takes only one existential variable ranging over "'a => 'b" to
6.123 ruin everything. Hence we do it only if there are few facts (which is
6.124 @@ -2614,32 +2612,45 @@
6.125 if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op
6.126 else
6.127 Sufficient_App_Op_And_Predicator
6.128 +
6.129 val lam_trans =
6.130 if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
6.131 else lam_trans
6.132 +
6.133 val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
6.134 translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts
6.135 +
6.136 val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts
6.137 - val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
6.138 val ctrss = all_ctrss_of_datatypes ctxt
6.139 +
6.140 fun firstorderize in_helper =
6.141 firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish
6.142 sym_tab0
6.143 +
6.144 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
6.145 val (ho_stuff, sym_tab) =
6.146 sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
6.147 + val helpers =
6.148 + sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
6.149 + |> map (firstorderize true)
6.150 +
6.151 + val all_facts = helpers @ conjs @ facts
6.152 + val mono = mononotonicity_info_of_facts ctxt type_enc completish all_facts
6.153 + val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
6.154 +
6.155 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
6.156 uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab
6.157 val (_, sym_tab) =
6.158 (ho_stuff, sym_tab)
6.159 |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
6.160 uncurried_alias_eq_tms
6.161 - val helpers =
6.162 - sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
6.163 - |> map (firstorderize true)
6.164 - val all_facts = helpers @ conjs @ facts
6.165 - val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
6.166 val datatypes = datatypes_of_sym_table ctxt ctrss format type_enc uncurried_aliases sym_tab
6.167 +
6.168 + val num_facts = length facts
6.169 + val freshen = mode <> Exporter andalso mode <> Translator
6.170 + val pos = mode <> Exporter
6.171 + val rank_of = rank_of_fact_num num_facts
6.172 +
6.173 val class_decl_lines = decl_lines_of_classes type_enc classes
6.174 val sym_decl_lines =
6.175 (conjs, helpers @ facts, uncurried_alias_eq_tms)
6.176 @@ -2647,22 +2658,18 @@
6.177 |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
6.178 val datatype_decl_lines = map decl_line_of_datatype datatypes
6.179 val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
6.180 - val num_facts = length facts
6.181 - val freshen = mode <> Exporter andalso mode <> Translator
6.182 - val pos = mode <> Exporter
6.183 - val rank_of = rank_of_fact_num num_facts
6.184 val fact_lines =
6.185 - map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
6.186 - (0 upto num_facts - 1 ~~ facts)
6.187 + map_index (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of) facts
6.188 val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
6.189 val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
6.190 val helper_lines =
6.191 - 0 upto length helpers - 1 ~~ helpers
6.192 - |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
6.193 + map_index (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
6.194 + helpers
6.195 val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
6.196 val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
6.197 +
6.198 (* Reordering these might confuse the proof reconstruction code. *)
6.199 - val problem =
6.200 + val (problem, pool) =
6.201 [(explicit_declsN, decl_lines),
6.202 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
6.203 (factsN, fact_lines),
6.204 @@ -2671,14 +2678,13 @@
6.205 (helpersN, helper_lines),
6.206 (free_typesN, free_type_lines),
6.207 (conjsN, conj_lines)]
6.208 - val problem =
6.209 - problem
6.210 |> (case format of
6.211 CNF => ensure_cnf_problem
6.212 | CNF_UEQ => filter_cnf_ueq_problem
6.213 | FOF => I
6.214 | _ => declare_undeclared_in_problem implicit_declsN)
6.215 - val (problem, pool) = problem |> nice_atp_problem readable_names format
6.216 + |> nice_atp_problem readable_names format
6.217 +
6.218 fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
6.219 in
6.220 (problem, Option.map snd pool |> the_default Symtab.empty, lifted,
6.221 @@ -2715,7 +2721,7 @@
6.222 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
6.223 / Real.fromInt num_facts
6.224 in
6.225 - map weight_of (0 upto num_facts - 1) ~~ facts
6.226 + map_index (apfst weight_of) facts
6.227 |> fold (uncurry add_line_weights)
6.228 end
6.229 val get = these o AList.lookup (op =) problem
7.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Jul 01 17:01:48 2014 +0200
7.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Jul 01 17:06:54 2014 +0200
7.3 @@ -190,10 +190,9 @@
7.4 (* Given the definition of a Skolem function, return a theorem to replace
7.5 an existential formula by a use of that function.
7.6 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
7.7 -fun old_skolem_theorem_of_def thy rhs0 =
7.8 +fun old_skolem_theorem_of_def ctxt rhs0 =
7.9 let
7.10 - val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
7.11 -
7.12 + val thy = Proof_Context.theory_of ctxt
7.13 val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
7.14 val rhs' = rhs |> Thm.dest_comb |> snd
7.15 val (ch, frees) = c_variant_abs_multi (rhs', [])
7.16 @@ -201,8 +200,7 @@
7.17 val T =
7.18 case hilbert of
7.19 Const (_, Type (@{type_name fun}, [_, T])) => T
7.20 - | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
7.21 - [hilbert])
7.22 + | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
7.23 val cex = cterm_of thy (HOLogic.exists_const T)
7.24 val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
7.25 val conc =
7.26 @@ -373,7 +371,7 @@
7.27 nnf_axiom choice_ths new_skolem ax_no th ctxt0
7.28 fun clausify th =
7.29 make_cnf (if new_skolem orelse null choice_ths then []
7.30 - else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
7.31 + else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
7.32 th ctxt ctxt
7.33 val (cnf_ths, ctxt) = clausify nnf_th
7.34 fun intr_imp ct th =
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 01 17:01:48 2014 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 01 17:06:54 2014 +0200
8.3 @@ -196,8 +196,11 @@
8.4 (facts |> map (fst o fst) |> space_implode " ") ^ "."
8.5
8.6 fun string_of_factss factss =
8.7 - if forall (null o snd) factss then "Found no relevant facts."
8.8 - else cat_lines (map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) factss)
8.9 + if forall (null o snd) factss then
8.10 + "Found no relevant facts."
8.11 + else
8.12 + cat_lines (map (fn (filter, facts) =>
8.13 + (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
8.14
8.15 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
8.16 output_result i (fact_override as {only, ...}) minimize_command state =
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 17:01:48 2014 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jul 01 17:06:54 2014 +0200
9.3 @@ -84,6 +84,7 @@
9.4 val risky_defs = @{thms Bit0_def Bit1_def}
9.5
9.6 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
9.7 +
9.8 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
9.9 | is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2
9.10 | is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
9.11 @@ -114,6 +115,7 @@
9.12 ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
9.13 | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
9.14 | normT (T as TFree _) = pair T
9.15 +
9.16 fun norm (t $ u) = norm t ##>> norm u #>> op $
9.17 | norm (Const (s, T)) = normT T #>> curry Const s
9.18 | norm (Var (z as (_, T))) =
9.19 @@ -164,6 +166,7 @@
9.20 val bracket =
9.21 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
9.22 |> implode
9.23 +
9.24 fun nth_name j =
9.25 (case xref of
9.26 Facts.Fact s => backquote s ^ bracket
9.27 @@ -173,12 +176,15 @@
9.28 | Facts.Named ((name, _), SOME intervals) =>
9.29 make_name reserved true
9.30 (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
9.31 +
9.32 fun add_nth th (j, rest) =
9.33 let val name = nth_name j in
9.34 (j + 1, ((name, stature_of_thm false [] chained css name th), th)
9.35 :: rest)
9.36 end
9.37 - in (0, []) |> fold add_nth ths |> snd end
9.38 + in
9.39 + (0, []) |> fold add_nth ths |> snd
9.40 + end
9.41
9.42 (* Reject theorems with names like "List.filter.filter_list_def" or
9.43 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
9.44 @@ -222,6 +228,7 @@
9.45
9.46 (* FIXME: make more reliable *)
9.47 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
9.48 +
9.49 fun is_low_level_class_const (s, _) =
9.50 s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
9.51
9.52 @@ -250,6 +257,7 @@
9.53 not (member (op =) atp_widely_irrelevant_consts s)
9.54 | is_interesting_subterm (Free _) = true
9.55 | is_interesting_subterm _ = false
9.56 +
9.57 fun interest_of_bool t =
9.58 if exists_Const (is_technical_const orf is_low_level_class_const orf
9.59 type_has_top_sort o snd) t then
9.60 @@ -259,6 +267,7 @@
9.61 Boring
9.62 else
9.63 Interesting
9.64 +
9.65 fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
9.66 | interest_of_prop Ts (@{const Pure.imp} $ t $ u) =
9.67 combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
9.68 @@ -269,6 +278,7 @@
9.69 | interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) =
9.70 combine_interests (interest_of_bool t) (interest_of_bool u)
9.71 | interest_of_prop _ _ = Deal_Breaker
9.72 +
9.73 val t = prop_of th
9.74 in
9.75 (interest_of_prop [] t <> Interesting andalso
9.76 @@ -277,11 +287,9 @@
9.77 end
9.78
9.79 fun is_blacklisted_or_something ctxt ho_atp =
9.80 - let
9.81 - val blist = multi_base_blacklist ctxt ho_atp
9.82 - fun is_blisted name =
9.83 - is_package_def name orelse exists (fn s => String.isSuffix s name) blist
9.84 - in is_blisted end
9.85 + let val blist = multi_base_blacklist ctxt ho_atp in
9.86 + fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
9.87 + end
9.88
9.89 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
9.90 they are displayed as "M" and we want to avoid clashes with these. But
9.91 @@ -316,6 +324,7 @@
9.92 let
9.93 fun add stature th =
9.94 Termtab.update (normalize_vars (prop_of th), stature)
9.95 +
9.96 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
9.97 ctxt |> claset_of |> Classical.rep_cs
9.98 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
9.99 @@ -331,18 +340,18 @@
9.100 |> filter_out (member Thm.eq_thm_prop risky_defs)
9.101 |> List.partition (is_rec_def o prop_of)
9.102 val spec_intros =
9.103 - specs |> filter (member (op =) [Spec_Rules.Inductive,
9.104 - Spec_Rules.Co_Inductive] o fst)
9.105 + specs |> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst)
9.106 |> maps (snd o snd)
9.107 in
9.108 - Termtab.empty |> fold (add Simp o snd) simps
9.109 - |> fold (add Rec_Def) rec_defs
9.110 - |> fold (add Non_Rec_Def) nonrec_defs
9.111 + Termtab.empty
9.112 + |> fold (add Simp o snd) simps
9.113 + |> fold (add Rec_Def) rec_defs
9.114 + |> fold (add Non_Rec_Def) nonrec_defs
9.115 (* Add once it is used:
9.116 - |> fold (add Elim) elims
9.117 + |> fold (add Elim) elims
9.118 *)
9.119 - |> fold (add Intro) intros
9.120 - |> fold (add Inductive) spec_intros
9.121 + |> fold (add Intro) intros
9.122 + |> fold (add Inductive) spec_intros
9.123 end
9.124 end
9.125
9.126 @@ -359,9 +368,8 @@
9.127 fun if_thm_before th th' =
9.128 if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
9.129
9.130 -(* Hack: Conflate the facts about a class as seen from the outside with the
9.131 - corresponding low-level facts, so that MaSh can learn from the low-level
9.132 - proofs. *)
9.133 +(* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
9.134 + facts, so that MaSh can learn from the low-level proofs. *)
9.135 fun un_class_ify s =
9.136 (case first_field "_class" s of
9.137 SOME (pref, suf) => [s, pref ^ suf]
9.138 @@ -407,6 +415,7 @@
9.139 fun varify_noninducts (t as Free (s, T)) =
9.140 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
9.141 | varify_noninducts t = t
9.142 +
9.143 val p_inst =
9.144 concl_prop |> map_aterms varify_noninducts |> close_form
9.145 |> lambda (Free ind_x)
9.146 @@ -455,40 +464,44 @@
9.147 val thy = Proof_Context.theory_of ctxt
9.148 val global_facts = Global_Theory.facts_of thy
9.149 val is_too_complex =
9.150 - if generous orelse
9.151 - fact_count global_facts >= max_facts_for_complex_check then
9.152 + if generous orelse fact_count global_facts >= max_facts_for_complex_check then
9.153 K false
9.154 else
9.155 is_too_complex
9.156 val local_facts = Proof_Context.facts_of ctxt
9.157 val named_locals = local_facts |> Facts.dest_static true [global_facts]
9.158 val assms = Assumption.all_assms_of ctxt
9.159 +
9.160 fun is_good_unnamed_local th =
9.161 not (Thm.has_name_hint th) andalso
9.162 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
9.163 +
9.164 val unnamed_locals =
9.165 union Thm.eq_thm_prop (Facts.props local_facts) chained
9.166 |> filter is_good_unnamed_local |> map (pair "" o single)
9.167 val full_space =
9.168 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
9.169 val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
9.170 +
9.171 fun add_facts global foldx facts =
9.172 foldx (fn (name0, ths) => fn accum =>
9.173 if name0 <> "" andalso
9.174 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
9.175 (Facts.is_concealed facts name0 orelse
9.176 + Long_Name.is_hidden (Facts.intern facts name0) orelse
9.177 (not generous andalso is_blacklisted_or_something name0)) then
9.178 accum
9.179 else
9.180 let
9.181 val n = length ths
9.182 val multi = n > 1
9.183 +
9.184 fun check_thms a =
9.185 (case try (Proof_Context.get_thms ctxt) a of
9.186 NONE => false
9.187 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
9.188 in
9.189 - snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) =>
9.190 + snd (fold_rev (fn th => fn (j, accum) =>
9.191 (j - 1,
9.192 if not (member Thm.eq_thm_prop add_ths th) andalso
9.193 (is_likely_tautology_too_meta_or_too_technical th orelse
9.194 @@ -496,21 +509,26 @@
9.195 accum
9.196 else
9.197 let
9.198 - val new =
9.199 - (((fn () =>
9.200 - if name0 = "" then
9.201 - backquote_thm ctxt th
9.202 - else
9.203 - [Facts.extern ctxt facts name0,
9.204 - Name_Space.extern ctxt full_space name0]
9.205 - |> find_first check_thms
9.206 - |> the_default name0
9.207 - |> make_name reserved multi j),
9.208 - stature_of_thm global assms chained css name0 th),
9.209 - th)
9.210 + fun get_name () =
9.211 + if name0 = "" then
9.212 + backquote_thm ctxt th
9.213 + else
9.214 + let val short_name = Facts.extern ctxt facts name0 in
9.215 + if check_thms short_name then
9.216 + short_name
9.217 + else
9.218 + let val long_name = Name_Space.extern ctxt full_space name0 in
9.219 + if check_thms long_name then
9.220 + long_name
9.221 + else
9.222 + name0
9.223 + end
9.224 + end
9.225 + |> make_name reserved multi j
9.226 + val stature = stature_of_thm global assms chained css name0 th
9.227 + val new = ((get_name, stature), th)
9.228 in
9.229 - if multi then (uni_accum, new :: multi_accum)
9.230 - else (new :: uni_accum, multi_accum)
9.231 + (if multi then apsnd else apfst) (cons new) accum
9.232 end)) ths (n, accum))
9.233 end)
9.234 in
9.235 @@ -522,8 +540,7 @@
9.236 |> op @
9.237 end
9.238
9.239 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
9.240 - concl_t =
9.241 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
9.242 if only andalso null add then
9.243 []
9.244 else
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Tue Jul 01 17:01:48 2014 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Tue Jul 01 17:06:54 2014 +0200
10.3 @@ -70,11 +70,10 @@
10.4 val thy = Proof_Context.theory_of ctxt
10.5 val get_types = post_fold_term_type (K cons) []
10.6 in
10.7 - fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
10.8 - handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
10.9 + fold (perhaps o try o Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
10.10 end
10.11
10.12 -fun handle_trivial_tfrees ctxt (t', subst) =
10.13 +fun handle_trivial_tfrees ctxt t' subst =
10.14 let
10.15 val add_tfree_names = snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
10.16
10.17 @@ -181,10 +180,10 @@
10.18 let
10.19 val t' = generalize_types ctxt t
10.20 val subst = match_types ctxt t' t
10.21 - val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
10.22 - val typing_spots = t' |> typing_spot_table |> reverse_greedy |> sort int_ord
10.23 + val (t'', subst') = handle_trivial_tfrees ctxt t' subst
10.24 + val typing_spots = t'' |> typing_spot_table |> reverse_greedy |> sort int_ord
10.25 in
10.26 - introduce_annotations subst typing_spots t t'
10.27 + introduce_annotations subst' typing_spots t t''
10.28 end
10.29
10.30 end;
11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 17:01:48 2014 +0200
11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 17:06:54 2014 +0200
11.3 @@ -34,17 +34,18 @@
11.4 val decode_strs : string -> string list
11.5
11.6 datatype mash_engine =
11.7 - MaSh_kNN
11.8 + MaSh_NB
11.9 + | MaSh_kNN
11.10 + | MaSh_NB_kNN
11.11 + | MaSh_NB_Ext
11.12 | MaSh_kNN_Ext
11.13 - | MaSh_NB
11.14 - | MaSh_NB_Ext
11.15
11.16 val is_mash_enabled : unit -> bool
11.17 val the_mash_engine : unit -> mash_engine
11.18
11.19 + val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
11.20 val nickname_of_thm : thm -> string
11.21 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
11.22 - val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
11.23 val crude_thm_ord : thm * thm -> order
11.24 val thm_less : thm * thm -> bool
11.25 val goal_of_thm : theory -> thm -> thm
11.26 @@ -138,36 +139,70 @@
11.27 end
11.28
11.29 datatype mash_engine =
11.30 - MaSh_kNN
11.31 + MaSh_NB
11.32 +| MaSh_kNN
11.33 +| MaSh_NB_kNN
11.34 +| MaSh_NB_Ext
11.35 | MaSh_kNN_Ext
11.36 -| MaSh_NB
11.37 -| MaSh_NB_Ext
11.38
11.39 fun mash_engine () =
11.40 let val flag1 = Options.default_string @{system_option MaSh} in
11.41 (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
11.42 - "yes" => SOME MaSh_NB
11.43 - | "sml" => SOME MaSh_NB
11.44 + "yes" => SOME MaSh_NB_kNN
11.45 + | "sml" => SOME MaSh_NB_kNN
11.46 + | "nb" => SOME MaSh_NB
11.47 | "knn" => SOME MaSh_kNN
11.48 + | "nb_knn" => SOME MaSh_NB_kNN
11.49 + | "nb_ext" => SOME MaSh_NB_Ext
11.50 | "knn_ext" => SOME MaSh_kNN_Ext
11.51 - | "nb" => SOME MaSh_NB
11.52 - | "nb_ext" => SOME MaSh_NB_Ext
11.53 - | _ => NONE)
11.54 + | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
11.55 end
11.56
11.57 val is_mash_enabled = is_some o mash_engine
11.58 -val the_mash_engine = the_default MaSh_NB o mash_engine
11.59 +val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
11.60
11.61 +fun scaled_avg [] = 0
11.62 + | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
11.63
11.64 -(*** Isabelle-agnostic machine learning ***)
11.65 +fun avg [] = 0.0
11.66 + | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
11.67
11.68 -structure MaSh =
11.69 -struct
11.70 +fun normalize_scores _ [] = []
11.71 + | normalize_scores max_facts xs =
11.72 + map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
11.73
11.74 -fun heap cmp bnd al a =
11.75 +fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
11.76 + distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
11.77 + | mesh_facts fact_eq max_facts mess =
11.78 + let
11.79 + val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
11.80 +
11.81 + fun score_in fact (global_weight, (sels, unks)) =
11.82 + let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
11.83 + (case find_index (curry fact_eq fact o fst) sels of
11.84 + ~1 => if member fact_eq unks fact then NONE else SOME 0.0
11.85 + | rank => score_at rank)
11.86 + end
11.87 +
11.88 + fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
11.89 + in
11.90 + fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
11.91 + |> map (`weight_of) |> sort (int_ord o pairself fst o swap)
11.92 + |> map snd |> take max_facts
11.93 + end
11.94 +
11.95 +fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *)
11.96 +fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *)
11.97 +
11.98 +fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
11.99 +fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
11.100 +
11.101 +fun rev_sort_array_prefix cmp bnd a =
11.102 let
11.103 exception BOTTOM of int
11.104
11.105 + val al = Array.length a
11.106 +
11.107 fun maxson l i =
11.108 let val i31 = i + i + i + 1 in
11.109 if i31 + 2 < l then
11.110 @@ -231,7 +266,17 @@
11.111 ()
11.112 end
11.113
11.114 -val number_of_nearest_neighbors = 10 (* FUDGE *)
11.115 +fun rev_sort_list_prefix cmp bnd xs =
11.116 + let val ary = Array.fromList xs in
11.117 + rev_sort_array_prefix cmp bnd ary;
11.118 + Array.foldr (op ::) [] ary
11.119 + end
11.120 +
11.121 +
11.122 +(*** Isabelle-agnostic machine learning ***)
11.123 +
11.124 +structure MaSh =
11.125 +struct
11.126
11.127 fun select_visible_facts big_number recommends =
11.128 List.app (fn at =>
11.129 @@ -239,78 +284,6 @@
11.130 Array.update (recommends, at, (j, big_number + ov))
11.131 end)
11.132
11.133 -fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats =
11.134 - let
11.135 - exception EXIT of unit
11.136 -
11.137 - val ln_afreq = Math.ln (Real.fromInt num_facts)
11.138 - fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
11.139 -
11.140 - val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
11.141 -
11.142 - fun do_feat (s, sw0) =
11.143 - let
11.144 - val sw = sw0 * tfidf s
11.145 - val w2 = sw * sw
11.146 -
11.147 - fun inc_overlap j =
11.148 - let val (_, ov) = Array.sub (overlaps_sqr, j) in
11.149 - Array.update (overlaps_sqr, j, (j, w2 + ov))
11.150 - end
11.151 - in
11.152 - List.app inc_overlap (Array.sub (feat_facts, s))
11.153 - end
11.154 -
11.155 - val _ = List.app do_feat goal_feats
11.156 - val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
11.157 - val no_recommends = Unsynchronized.ref 0
11.158 - val recommends = Array.tabulate (num_facts, rpair 0.0)
11.159 - val age = Unsynchronized.ref 500000000.0
11.160 -
11.161 - fun inc_recommend j v =
11.162 - let val (_, ov) = Array.sub (recommends, j) in
11.163 - if ov <= 0.0 then
11.164 - (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
11.165 - else if ov < !age + 1000.0 then
11.166 - Array.update (recommends, j, (j, v + ov))
11.167 - else
11.168 - ()
11.169 - end
11.170 -
11.171 - val k = Unsynchronized.ref 0
11.172 - fun do_k k =
11.173 - if k >= num_facts then
11.174 - raise EXIT ()
11.175 - else
11.176 - let
11.177 - val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
11.178 - val o1 = Math.sqrt o2
11.179 - val _ = inc_recommend j o1
11.180 - val ds = Vector.sub (depss, j)
11.181 - val l = Real.fromInt (length ds)
11.182 - in
11.183 - List.app (fn d => inc_recommend d (o1 / l)) ds
11.184 - end
11.185 -
11.186 - fun while1 () =
11.187 - if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
11.188 - handle EXIT () => ()
11.189 -
11.190 - fun while2 () =
11.191 - if !no_recommends >= max_suggs then ()
11.192 - else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
11.193 - handle EXIT () => ()
11.194 -
11.195 - fun ret acc at =
11.196 - if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
11.197 - in
11.198 - while1 ();
11.199 - while2 ();
11.200 - select_visible_facts 1000000000.0 recommends visible_facts;
11.201 - heap (Real.compare o pairself snd) max_suggs num_facts recommends;
11.202 - ret [] (Integer.max 0 (num_facts - max_suggs))
11.203 - end
11.204 -
11.205 fun wider_array_of_vector init vec =
11.206 let val ary = Array.array init in
11.207 Array.copyVec {src = vec, dst = ary, di = 0};
11.208 @@ -389,10 +362,88 @@
11.209 if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
11.210 in
11.211 select_visible_facts 100000.0 posterior visible_facts;
11.212 - heap (Real.compare o pairself snd) max_suggs num_facts posterior;
11.213 + rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior;
11.214 ret (Integer.max 0 (num_facts - max_suggs)) []
11.215 end
11.216
11.217 +val number_of_nearest_neighbors = 10 (* FUDGE *)
11.218 +
11.219 +fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
11.220 + let
11.221 + exception EXIT of unit
11.222 +
11.223 + val ln_afreq = Math.ln (Real.fromInt num_facts)
11.224 + fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
11.225 +
11.226 + val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
11.227 +
11.228 + val feat_facts = Array.array (num_feats, [])
11.229 + val _ = Vector.foldl (fn (feats, fact) =>
11.230 + (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1)) 0 featss
11.231 +
11.232 + fun do_feat (s, sw0) =
11.233 + let
11.234 + val sw = sw0 * tfidf s
11.235 + val w2 = sw * sw
11.236 +
11.237 + fun inc_overlap j =
11.238 + let val (_, ov) = Array.sub (overlaps_sqr, j) in
11.239 + Array.update (overlaps_sqr, j, (j, w2 + ov))
11.240 + end
11.241 + in
11.242 + List.app inc_overlap (Array.sub (feat_facts, s))
11.243 + end
11.244 +
11.245 + val _ = List.app do_feat goal_feats
11.246 + val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr
11.247 + val no_recommends = Unsynchronized.ref 0
11.248 + val recommends = Array.tabulate (num_facts, rpair 0.0)
11.249 + val age = Unsynchronized.ref 500000000.0
11.250 +
11.251 + fun inc_recommend v j =
11.252 + let val (_, ov) = Array.sub (recommends, j) in
11.253 + if ov <= 0.0 then
11.254 + (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
11.255 + else if ov < !age + 1000.0 then
11.256 + Array.update (recommends, j, (j, v + ov))
11.257 + else
11.258 + ()
11.259 + end
11.260 +
11.261 + val k = Unsynchronized.ref 0
11.262 + fun do_k k =
11.263 + if k >= num_facts then
11.264 + raise EXIT ()
11.265 + else
11.266 + let
11.267 + val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
11.268 + val o1 = Math.sqrt o2
11.269 + val _ = inc_recommend o1 j
11.270 + val ds = Vector.sub (depss, j)
11.271 + val l = Real.fromInt (length ds)
11.272 + in
11.273 + List.app (inc_recommend (o1 / l)) ds
11.274 + end
11.275 +
11.276 + fun while1 () =
11.277 + if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
11.278 + handle EXIT () => ()
11.279 +
11.280 + fun while2 () =
11.281 + if !no_recommends >= max_suggs then ()
11.282 + else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
11.283 + handle EXIT () => ()
11.284 +
11.285 + fun ret acc at =
11.286 + if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
11.287 + in
11.288 + while1 ();
11.289 + while2 ();
11.290 + select_visible_facts 1000000000.0 recommends visible_facts;
11.291 + rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends;
11.292 + ret [] (Integer.max 0 (num_facts - max_suggs))
11.293 + end
11.294 +
11.295 (* experimental *)
11.296 fun external_tool tool max_suggs learns goal_feats =
11.297 let
11.298 @@ -435,26 +486,35 @@
11.299 fun query_external ctxt engine max_suggs learns goal_feats =
11.300 (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
11.301 (case engine of
11.302 - MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats
11.303 - | MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats))
11.304 + MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
11.305 + | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
11.306
11.307 fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
11.308 (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
11.309 - (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
11.310 - elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
11.311 - (case engine of
11.312 - MaSh_kNN =>
11.313 - let
11.314 - val feat_facts = Array.array (num_feats, [])
11.315 - val _ =
11.316 - Vector.foldl (fn (feats, fact) =>
11.317 - (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1))
11.318 - 0 featss
11.319 - in
11.320 - k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts int_goal_feats
11.321 - end
11.322 - | MaSh_NB => naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats)
11.323 - |> map (curry Vector.sub fact_names o fst))
11.324 + let
11.325 + fun nb () =
11.326 + naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats
11.327 + |> map fst
11.328 + fun knn () =
11.329 + k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts
11.330 + int_goal_feats
11.331 + |> map fst
11.332 + in
11.333 + (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
11.334 + elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
11.335 + (case engine of
11.336 + MaSh_NB => nb ()
11.337 + | MaSh_kNN => knn ()
11.338 + | MaSh_NB_kNN =>
11.339 + let
11.340 + val mess =
11.341 + [(0.5 (* FUDGE *), (weight_facts_steeply (nb ()), [])),
11.342 + (0.5 (* FUDGE *), (weight_facts_steeply (knn ()), []))]
11.343 + in
11.344 + mesh_facts (op =) max_suggs mess
11.345 + end)
11.346 + |> map (curry Vector.sub fact_names))
11.347 + end
11.348
11.349 end;
11.350
11.351 @@ -481,7 +541,7 @@
11.352 val decode_str = String.explode #> unmeta_chars []
11.353
11.354 val encode_strs = map encode_str #> space_implode " "
11.355 -val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
11.356 +val decode_strs = space_explode " " #> map decode_str
11.357
11.358 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
11.359
11.360 @@ -706,36 +766,6 @@
11.361 |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
11.362 in map_filter lookup end
11.363
11.364 -fun scaled_avg [] = 0
11.365 - | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
11.366 -
11.367 -fun avg [] = 0.0
11.368 - | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
11.369 -
11.370 -fun normalize_scores _ [] = []
11.371 - | normalize_scores max_facts xs =
11.372 - map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
11.373 -
11.374 -fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
11.375 - distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
11.376 - | mesh_facts fact_eq max_facts mess =
11.377 - let
11.378 - val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
11.379 -
11.380 - fun score_in fact (global_weight, (sels, unks)) =
11.381 - let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
11.382 - (case find_index (curry fact_eq fact o fst) sels of
11.383 - ~1 => if member fact_eq unks fact then NONE else SOME 0.0
11.384 - | rank => score_at rank)
11.385 - end
11.386 -
11.387 - fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
11.388 - in
11.389 - fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
11.390 - |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
11.391 - |> map snd |> take max_facts
11.392 - end
11.393 -
11.394 fun free_feature_of s = "f" ^ s
11.395 fun thy_feature_of s = "y" ^ s
11.396 fun type_feature_of s = "t" ^ s
11.397 @@ -1088,9 +1118,13 @@
11.398 find_maxes Symtab.empty ([], Graph.maximals G)
11.399 end
11.400
11.401 -fun maximal_wrt_access_graph access_G facts =
11.402 - map (nickname_of_thm o snd) facts
11.403 - |> maximal_wrt_graph access_G
11.404 +fun maximal_wrt_access_graph _ [] = []
11.405 + | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
11.406 + let val thy = theory_of_thm th in
11.407 + fact :: filter_out (fn (_, th') => Theory.subthy (theory_of_thm th', thy)) facts
11.408 + |> map (nickname_of_thm o snd)
11.409 + |> maximal_wrt_graph access_G
11.410 + end
11.411
11.412 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
11.413
11.414 @@ -1098,20 +1132,6 @@
11.415 val extra_feature_factor = 0.1 (* FUDGE *)
11.416 val num_extra_feature_facts = 10 (* FUDGE *)
11.417
11.418 -(* FUDGE *)
11.419 -fun weight_of_proximity_fact rank =
11.420 - Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
11.421 -
11.422 -fun weight_facts_smoothly facts =
11.423 - facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
11.424 -
11.425 -(* FUDGE *)
11.426 -fun steep_weight_of_fact rank =
11.427 - Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
11.428 -
11.429 -fun weight_facts_steeply facts =
11.430 - facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
11.431 -
11.432 val max_proximity_facts = 100
11.433
11.434 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
11.435 @@ -1136,8 +1156,11 @@
11.436 val thy_name = Context.theory_name thy
11.437 val engine = the_mash_engine ()
11.438
11.439 - val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
11.440 - val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
11.441 + val facts = facts
11.442 + |> rev_sort_list_prefix (crude_thm_ord o pairself snd)
11.443 + (Int.max (num_extra_feature_facts, max_proximity_facts))
11.444 +
11.445 + val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
11.446
11.447 fun fact_has_right_theory (_, th) =
11.448 thy_name = Context.theory_name (theory_of_thm th)
11.449 @@ -1147,53 +1170,44 @@
11.450 |> features_of ctxt (theory_of_thm th) stature
11.451 |> map (rpair (weight * factor))
11.452
11.453 - fun query_args access_G =
11.454 - let
11.455 - val parents = maximal_wrt_access_graph access_G facts
11.456 -
11.457 - val goal_feats = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
11.458 - val chained_feats = chained
11.459 - |> map (rpair 1.0)
11.460 - |> map (chained_or_extra_features_of chained_feature_factor)
11.461 - |> rpair [] |-> fold (union (eq_fst (op =)))
11.462 - val extra_feats =
11.463 - facts
11.464 - |> take (Int.max (0, num_extra_feature_facts - length chained))
11.465 - |> filter fact_has_right_theory
11.466 - |> weight_facts_steeply
11.467 - |> map (chained_or_extra_features_of extra_feature_factor)
11.468 - |> rpair [] |-> fold (union (eq_fst (op =)))
11.469 - val feats =
11.470 - fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats)
11.471 - |> debug ? sort (Real.compare o swap o pairself snd)
11.472 - in
11.473 - (parents, feats)
11.474 - end
11.475 -
11.476 val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
11.477 peek_state ctxt
11.478
11.479 + val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
11.480 + val chained_feats = chained
11.481 + |> map (rpair 1.0)
11.482 + |> map (chained_or_extra_features_of chained_feature_factor)
11.483 + |> rpair [] |-> fold (union (eq_fst (op =)))
11.484 + val extra_feats = facts
11.485 + |> take (Int.max (0, num_extra_feature_facts - length chained))
11.486 + |> filter fact_has_right_theory
11.487 + |> weight_facts_steeply
11.488 + |> map (chained_or_extra_features_of extra_feature_factor)
11.489 + |> rpair [] |-> fold (union (eq_fst (op =)))
11.490 +
11.491 + val goal_feats =
11.492 + fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
11.493 + |> debug ? sort (Real.compare o swap o pairself snd)
11.494 +
11.495 + val parents = maximal_wrt_access_graph access_G facts
11.496 + val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
11.497 +
11.498 val suggs =
11.499 - let
11.500 - val (parents, goal_feats) = query_args access_G
11.501 - val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
11.502 - in
11.503 - if engine = MaSh_kNN_Ext orelse engine = MaSh_NB_Ext then
11.504 - let
11.505 - val learns =
11.506 - Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
11.507 - in
11.508 - MaSh.query_external ctxt engine max_suggs learns goal_feats
11.509 - end
11.510 - else
11.511 - let
11.512 - val int_goal_feats =
11.513 - map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
11.514 - in
11.515 - MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
11.516 - goal_feats int_goal_feats
11.517 - end
11.518 - end
11.519 + if engine = MaSh_NB_Ext orelse engine = MaSh_kNN_Ext then
11.520 + let
11.521 + val learns =
11.522 + Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
11.523 + in
11.524 + MaSh.query_external ctxt engine max_suggs learns goal_feats
11.525 + end
11.526 + else
11.527 + let
11.528 + val int_goal_feats =
11.529 + map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
11.530 + in
11.531 + MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
11.532 + goal_feats int_goal_feats
11.533 + end
11.534
11.535 val unknown = filter_out (is_fact_in_graph access_G o snd) facts
11.536 in
11.537 @@ -1256,6 +1270,7 @@
11.538 let
11.539 val thy = Proof_Context.theory_of ctxt
11.540 val feats = features_of ctxt thy (Local, General) [t]
11.541 + val facts = rev_sort_list_prefix (crude_thm_ord o pairself snd) 1 facts
11.542 in
11.543 map_state ctxt
11.544 (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
11.545 @@ -1587,7 +1602,6 @@
11.546 end
11.547
11.548 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
11.549 -
11.550 fun running_learners () = Async_Manager.running_threads MaShN "learner"
11.551
11.552 end;
12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jul 01 17:01:48 2014 +0200
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jul 01 17:06:54 2014 +0200
12.3 @@ -76,6 +76,7 @@
12.4 | is_proof_method_direct Meson_Method = true
12.5 | is_proof_method_direct SMT2_Method = true
12.6 | is_proof_method_direct Simp_Method = true
12.7 + | is_proof_method_direct Simp_Size_Method = true
12.8 | is_proof_method_direct _ = false
12.9
12.10 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
12.11 @@ -103,7 +104,7 @@
12.12 maybe_paren (space_implode " " (meth_s :: ss))
12.13 end
12.14
12.15 -val silence_unifier = Try0.silence_methods false
12.16 +val silence_methods = Try0.silence_methods false
12.17
12.18 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
12.19 Method.insert_tac local_facts THEN'
12.20 @@ -113,22 +114,22 @@
12.21 Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
12.22 (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
12.23 end
12.24 - | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
12.25 + | Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts
12.26 | SMT2_Method =>
12.27 let val ctxt = Config.put SMT2_Config.verbose false ctxt in
12.28 SMT2_Solver.smt2_tac ctxt global_facts
12.29 end
12.30 - | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
12.31 + | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
12.32 + | Simp_Size_Method =>
12.33 + Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps @{thms size_ne_size_imp_ne})
12.34 | _ =>
12.35 Method.insert_tac global_facts THEN'
12.36 (case meth of
12.37 SATx_Method => SAT.satx_tac ctxt
12.38 | Blast_Method => blast_tac ctxt
12.39 - | Simp_Size_Method =>
12.40 - Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
12.41 - | Auto_Method => K (Clasimp.auto_tac (silence_unifier ctxt))
12.42 - | Fastforce_Method => Clasimp.fast_force_tac (silence_unifier ctxt)
12.43 - | Force_Method => Clasimp.force_tac (silence_unifier ctxt)
12.44 + | Auto_Method => K (Clasimp.auto_tac (silence_methods ctxt))
12.45 + | Fastforce_Method => Clasimp.fast_force_tac (silence_methods ctxt)
12.46 + | Force_Method => Clasimp.force_tac (silence_methods ctxt)
12.47 | Linarith_Method =>
12.48 let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
12.49 | Presburger_Method => Cooper.tac true [] [] ctxt
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 17:01:48 2014 +0200
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 17:06:54 2014 +0200
13.3 @@ -383,7 +383,7 @@
13.4 val atp_proof =
13.5 atp_proof
13.6 |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab
13.7 - |> introduce_spass_skolem
13.8 + |> spass ? introduce_spass_skolem
13.9 |> factify_atp_proof (map fst used_from) hyp_ts concl_t
13.10 in
13.11 (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
14.1 --- a/src/HOL/Tools/etc/options Tue Jul 01 17:01:48 2014 +0200
14.2 +++ b/src/HOL/Tools/etc/options Tue Jul 01 17:06:54 2014 +0200
14.3 @@ -36,4 +36,4 @@
14.4 -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
14.5
14.6 public option MaSh : string = "sml"
14.7 - -- "machine learning engine to use by Sledgehammer (sml, nb, knn, none)"
14.8 + -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"