# HG changeset patch # User wenzelm # Date 1391453438 -3600 # Node ID b1ca6ce9e1e0c8e1be07ac2a307f31801214ca87 # Parent 70e7ac6af16f70e010383390ac2d0bbfbfa1c667# Parent c3bb1cffce26cc718c16b736b7f01e6ee94fa686 merged; diff -r 70e7ac6af16f -r b1ca6ce9e1e0 NEWS --- a/NEWS Mon Feb 03 19:50:16 2014 +0100 +++ b/NEWS Mon Feb 03 19:50:38 2014 +0100 @@ -115,6 +115,8 @@ * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy * Sledgehammer: + - New option: + smt_proofs - Renamed options: isar_compress ~> compress_isar isar_try0 ~> try0_isar diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 19:50:38 2014 +0100 @@ -1103,7 +1103,7 @@ Pattern matching is only available for the argument on which the recursion takes place. Fortunately, it is easy to generate pattern-maching equations using the \keyw{simps\_of\_case} command provided by the theory -\verb|~~/src/HOL/Library/Simps_Case_Conv|. +\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|. *} simps_of_case at_simps: at.simps diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Doc/Datatypes/document/root.tex Mon Feb 03 19:50:38 2014 +0100 @@ -1,4 +1,5 @@ \documentclass[12pt,a4paper]{article} % fleqn +\usepackage[T1]{fontenc} \usepackage{cite} \usepackage{enumitem} \usepackage{footmisc} @@ -17,6 +18,8 @@ \setcounter{secnumdepth}{3} \setcounter{tocdepth}{3} +\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} + \newbox\boxA \setbox\boxA=\hbox{\ } \parindent=4\wd\boxA @@ -52,6 +55,9 @@ Dmitriy Traytel \\ {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ \hbox{}} + +\urlstyle{tt} + \begin{document} \maketitle diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Feb 03 19:50:38 2014 +0100 @@ -2640,9 +2640,11 @@ \item @{command (HOL) "code_identifier"} associates a a series of symbols (constants, type constructors, classes, class relations, instances, module names) with target-specific hints how these symbols shall be named. - \emph{Warning:} These hints are still subject to name disambiguation. + These hints gain precedence over names for symbols with no hints at all. + Conflicting hints are subject to name disambiguation. @{command (HOL) "code_modulename"} is a legacy variant for - @{command (HOL) "code_identifier"} on module names. It is at the discretion + @{command (HOL) "code_identifier"} on module names. + \emph{Warning:} It is at the discretion of the user to ensure that name prefixes of identifiers in compound statements like type classes or datatypes are still the same. diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Doc/Nitpick/document/root.tex Mon Feb 03 19:50:38 2014 +0100 @@ -40,6 +40,8 @@ \urlstyle{tt} +\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} + \begin{document} %%% TYPESETTING @@ -127,7 +129,7 @@ To run Nitpick, you must also make sure that the theory \textit{Nitpick} is imported---this is rarely a problem in practice since it is part of \textit{Main}. The examples presented in this manual can be found -in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory. +in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory. The known bugs and limitations at the time of writing are listed in \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either the tool or the manual should be directed to the author at \authoremail. diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 19:50:38 2014 +0100 @@ -42,6 +42,8 @@ \urlstyle{tt} +\renewcommand\_{\hbox{\textunderscore\kern-.05ex}} + \begin{document} %%% TYPESETTING @@ -115,7 +117,7 @@ The result of a successful proof search is some source text that usually (but not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed -proof relies on the general-purpose \textit{metis} proof method, which +proof typically relies on the general-purpose \textit{metis} proof method, which integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. @@ -294,7 +296,7 @@ Waldmeister is run only for unit equational problems, where the goal's conclusion is a (universally quantified) equation. -For each successful prover, Sledgehammer gives a one-liner \textit{metis} or +For each successful prover, Sledgehammer gives a one-line \textit{metis} or \textit{smt} method call. Rough timings are shown in parentheses, indicating how fast the call is. You can click the proof to insert it into the theory text. @@ -306,7 +308,7 @@ \postw When Isar proof construction is successful, it can yield proofs that are more -readable and also faster than the \textit{metis} or \textit{smt} one-liners. +readable and also faster than the \textit{metis} or \textit{smt} one-line proofs. This feature is experimental and is only available for ATPs. \section{Hints} @@ -357,7 +359,7 @@ if that helps. \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies -that Isar proofs should be generated, in addition to one-liner \textit{metis} or +that Isar proofs should be generated, in addition to one-line \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting \textit{compress\_isar} (\S\ref{output-format}). @@ -461,9 +463,8 @@ \begin{enum} \item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to -obtain a step-by-step Isar proof where each step is justified by \textit{metis}. -Since the steps are fairly small, \textit{metis} is more likely to be able to -replay them. +obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis} +and the other Isabelle proof methods are more likely to be able to replay them. \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It is usually stronger, but you need to either have Z3 available to replay the @@ -523,8 +524,8 @@ versions of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in -higher-order places (e.g., in set comprehensions). The method kicks in -automatically as a fallback when \textit{metis} fails, and it is sometimes +higher-order places (e.g., in set comprehensions). The method is automatically +tried as a fallback when \textit{metis} fails, and it is sometimes generated by Sledgehammer instead of \textit{metis} if the proof obviously requires type information or if \textit{metis} failed when Sledgehammer preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with @@ -1067,9 +1068,9 @@ \opdefault{max\_facts}{smart\_int}{smart} Specifies the maximum number of facts that may be returned by the relevance -filter. If the option is set to \textit{smart}, it is set to a value that was -empirically found to be appropriate for the prover. Typical values range between -50 and 1000. +filter. If the option is set to \textit{smart} (the default), it effectively +takes a value that was empirically found to be appropriate for the prover. +Typical values range between 50 and 1000. For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover}, \textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the @@ -1093,9 +1094,9 @@ Specifies the maximum number of monomorphic instances to generate beyond \textit{max\_facts}. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the -type encoding used. If the option is set to \textit{smart}, it is set to a value -that was empirically found to be appropriate for the prover. For most provers, -this value is 100. +type encoding used. If the option is set to \textit{smart} (the default), it +takes a value that was empirically found to be appropriate for the prover. For +most provers, this value is 100. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} @@ -1104,9 +1105,9 @@ Specifies the maximum number of iterations for the monomorphization fixpoint construction. The higher this limit is, the more monomorphic instances are potentially generated. Whether monomorphization takes place depends on the -type encoding used. If the option is set to \textit{smart}, it is set to a value -that was empirically found to be appropriate for the prover. For most provers, -this value is 3. +type encoding used. If the option is set to \textit{smart} (the default), it +takes a value that was empirically found to be appropriate for the prover. +For most provers, this value is 3. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).} @@ -1296,12 +1297,11 @@ \textit{overlord} (\S\ref{mode-of-operation}).} \opsmart{isar\_proofs}{no\_isar\_proofs} -Specifies whether Isar proofs should be output in addition to one-liner -\textit{metis} proofs. The construction of Isar proof is still experimental and -may sometimes fail; however, when they succeed they are usually faster and more -intelligible than \textit{metis} proofs. If the option is set to \textit{smart} -(the default), Isar proofs are only generated when no working one-liner -\textit{metis} proof is available. +Specifies whether Isar proofs should be output in addition to one-line proofs. +The construction of Isar proof is still experimental and may sometimes fail; +however, when they succeed they are usually faster and more intelligible than +one-line proofs. If the option is set to \textit{smart} (the default), Isar +proofs are only generated when no working one-line proof is available. \opdefault{compress\_isar}{int}{\upshape 10} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} @@ -1313,9 +1313,14 @@ \optrue{try0\_isar}{dont\_try0\_isar} Specifies whether standard proof methods such as \textit{auto} and -\textit{blast} should be tried as alternatives to \textit{metis} and -\textit{smt} in Isar proofs. The collection of methods is roughly the same as -for the \textbf{try0} command. +\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs. +The collection of methods is roughly the same as for the \textbf{try0} command. + +\opsmart{smt\_proofs}{no\_smt\_proofs} +Specifies whether the \textit{smt} proof method should be tried as an +alternative to \textit{metis}. If the option is set to \textit{smart} (the +default), the \textit{smt} method is used for one-line proofs but not in Isar +proofs. \end{enum} \subsection{Authentication} @@ -1351,10 +1356,10 @@ searching for a proof. This excludes problem preparation and is a soft limit. \opdefault{preplay\_timeout}{float}{\upshape 2} -Specifies the maximum number of seconds that \textit{metis} or \textit{smt} -should spend trying to ``preplay'' the found proof. If this option is set to 0, -no preplaying takes place, and no timing information is displayed next to the -suggested \textit{metis} calls. +Specifies the maximum number of seconds that \textit{metis} or other proof +methods should spend trying to ``preplay'' the found proof. If this option +is set to 0, no preplaying takes place, and no timing information is displayed +next to the suggested proof method calls. \nopagebreak {\small See also \textit{minimize} (\S\ref{mode-of-operation}).} diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Feb 03 19:50:38 2014 +0100 @@ -19,7 +19,7 @@ (*refers to minimization attempted by Mirabelle*) val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*) -val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) +val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) @@ -43,8 +43,7 @@ fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " -fun reconstructor_tag reconstructor id = - "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " +fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " val separator = "-----" @@ -130,16 +129,16 @@ proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) -datatype reconstructor_mode = +datatype proof_method_mode = Unminimized | Minimized | UnminimizedFT | MinimizedFT datatype data = Data of { sh: sh_data, min: min_data, - re_u: re_data, (* reconstructor with unminimized set of lemmas *) - re_m: re_data, (* reconstructor with minimized set of lemmas *) - re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *) - re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *) + re_u: re_data, (* proof method with unminimized set of lemmas *) + re_m: re_data, (* proof method with minimized set of lemmas *) + re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *) + re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *) mini: bool (* with minimization *) } @@ -218,39 +217,39 @@ fun inc_min_ab_ratios r = map_min_data (fn (succs, ab_ratios) => (succs, ab_ratios+r)) -val inc_reconstructor_calls = map_re_data +val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_success = map_re_data +val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_nontriv_calls = map_re_data +val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_nontriv_success = map_re_data +val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) -val inc_reconstructor_proofs = map_re_data +val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) -fun inc_reconstructor_time m t = map_re_data +fun inc_proof_method_time m t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m -val inc_reconstructor_timeout = map_re_data +val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) -fun inc_reconstructor_lemmas m n = map_re_data +fun inc_proof_method_lemmas m n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m -fun inc_reconstructor_posns m pos = map_re_data +fun inc_proof_method_posns m pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m @@ -292,19 +291,19 @@ fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, re_nontriv_success, re_proofs, re_time, re_timeout, (lemmas, lems_sos, lems_max), re_posns) = - (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls); - log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^ + (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); + log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ " (proof: " ^ str re_proofs ^ ")"); - log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout); + log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); - log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls); - log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^ + log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); + log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ " (proof: " ^ str re_proofs ^ ")"); - log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas); - log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos); - log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max); - log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time)); - log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^ + log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); + log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); + log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); + log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); + log ("Average time for successful " ^ tag ^ "proof method calls: " ^ str3 (avg_time re_time re_success)); if tag="" then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) @@ -325,7 +324,7 @@ fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () fun log_re tag m = log_re_data log tag sh_calls (tuple_of_re_data m) - fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () => + fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () => (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2))) in if sh_calls > 0 @@ -334,14 +333,14 @@ log_sh_data log (tuple_of_sh_data sh); log ""; if not mini - then log_reconstructor ("", re_u) ("fully-typed ", re_uft) + then log_proof_method ("", re_u) ("fully-typed ", re_uft) else app_if re_u (fn () => - (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft); + (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft); log ""; app_if re_m (fn () => (log_min_data log (tuple_of_min_data min); log ""; - log_reconstructor ("", re_m) ("fully-typed ", re_mft)))))) + log_proof_method ("", re_m) ("fully-typed ", re_mft)))))) else () end @@ -385,8 +384,8 @@ andalso not (String.isSubstring "may fail" s) (* Fragile hack *) -fun reconstructor_from_msg args msg = - (case AList.lookup (op =) args reconstructorK of +fun proof_method_from_msg args msg = + (case AList.lookup (op =) args proof_methodK of SOME name => name | NONE => if exists good_line (split_lines msg) then @@ -460,8 +459,8 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, - preplay = Lazy.value (Sledgehammer_Prover.plain_metis, - Sledgehammer_Reconstructor.Play_Failed), + preplay = Lazy.value (Sledgehammer_Proof_Methods.Metis_Method (NONE, NONE), + Sledgehammer_Proof_Methods.Play_Failed), message = K "", message_tail = ""}, ~1) val ({outcome, used_facts, run_time, preplay, message, message_tail, ...} : Sledgehammer_Prover.prover_result, @@ -501,7 +500,7 @@ in -fun run_sledgehammer trivial args reconstructor named_thms id +fun run_sledgehammer trivial args proof_method named_thms id ({pre=st, log, pos, ...}: Mirabelle.run_args) = let val thy = Proof.theory_of st @@ -557,7 +556,7 @@ change_data id (inc_sh_max_lems (length names)); change_data id (inc_sh_time_isa time_isa); change_data id (inc_sh_time_prover time_prover); - reconstructor := reconstructor_from_msg args msg; + proof_method := proof_method_from_msg args msg; named_thms := SOME (map_filter get_thms names); log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) @@ -572,7 +571,7 @@ end -fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = +fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) = let val thy = Proof.theory_of st val {goal, ...} = Proof.goal st @@ -614,7 +613,7 @@ change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); if length named_thms' = n0 then log (minimize_tag id ^ "already minimal") - else (reconstructor := reconstructor_from_msg args msg; + else (meth := proof_method_from_msg args msg; named_thms := SOME named_thms'; log (minimize_tag id ^ "succeeded:\n" ^ msg)) ) @@ -629,10 +628,10 @@ ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] -fun run_reconstructor trivial full m name reconstructor named_thms id +fun run_proof_method trivial full m name meth named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let - fun do_reconstructor named_thms ctxt = + fun do_method named_thms ctxt = let val ref_of_str = suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm @@ -646,56 +645,56 @@ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override in - if !reconstructor = "sledgehammer_tac" then + if !meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Systems.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms - else if !reconstructor = "smt" then + else if !meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if String.isPrefix "metis (" (!reconstructor) then + else if String.isPrefix "metis (" (!meth) then let val (type_encs, lam_trans) = - !reconstructor + !meth |> Outer_Syntax.scan Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end - else if !reconstructor = "metis" then + else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else K all_tac end - fun apply_reconstructor named_thms = - Mirabelle.can_apply timeout (do_reconstructor named_thms) st + fun apply_method named_thms = + Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" - | with_time (true, t) = (change_data id (inc_reconstructor_success m); + | with_time (true, t) = (change_data id (inc_proof_method_success m); if trivial then () - else change_data id (inc_reconstructor_nontriv_success m); - change_data id (inc_reconstructor_lemmas m (length named_thms)); - change_data id (inc_reconstructor_time m t); - change_data id (inc_reconstructor_posns m (pos, trivial)); - if name = "proof" then change_data id (inc_reconstructor_proofs m) else (); + else change_data id (inc_proof_method_nontriv_success m); + change_data id (inc_proof_method_lemmas m (length named_thms)); + change_data id (inc_proof_method_time m t); + change_data id (inc_proof_method_posns m (pos, trivial)); + if name = "proof" then change_data id (inc_proof_method_proofs m) else (); "succeeded (" ^ string_of_int t ^ ")") - fun timed_reconstructor named_thms = - (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) - handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false)) + fun timed_method named_thms = + (with_time (Mirabelle.cpu_time apply_method named_thms), true) + handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) val _ = log separator - val _ = change_data id (inc_reconstructor_calls m) - val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m) + val _ = change_data id (inc_proof_method_calls m) + val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m) in named_thms - |> timed_reconstructor - |>> log o prefix (reconstructor_tag reconstructor id) + |> timed_method + |>> log o prefix (proof_method_tag meth id) |> snd end @@ -717,7 +716,7 @@ if !num_sledgehammer_calls > max_calls then () else let - val reconstructor = Unsynchronized.ref "" + val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val minimize = AList.defined (op =) args minimizeK @@ -728,33 +727,28 @@ Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle TimeLimit.TimeOut => false else false - fun apply_reconstructor m1 m2 = + fun apply_method m1 m2 = if metis_ft then - if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st) + if not (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st) then - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial true m2 name reconstructor - (these (!named_thms))) id st; ()) + (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ()) else () else - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st; ()) + (Mirabelle.catch_result (proof_method_tag meth) false + (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ()) in change_data id (set_mini minimize); - Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor - named_thms) id st; + Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; if is_some (!named_thms) then - (apply_reconstructor Unminimized UnminimizedFT; + (apply_method Unminimized UnminimizedFT; if minimize andalso not (null (these (!named_thms))) then - (Mirabelle.catch minimize_tag - (run_minimize args reconstructor named_thms) id st; - apply_reconstructor Minimized MinimizedFT) + (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st; + apply_method Minimized MinimizedFT) else ()) else () end diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Feb 03 19:50:38 2014 +0100 @@ -17,7 +17,7 @@ ML_file "Tools/Sledgehammer/async_manager.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" -ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML" +ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML" ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML" diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 03 19:50:38 2014 +0100 @@ -28,9 +28,9 @@ val partial_type_encs : string list val default_metis_lam_trans : string - val metis_call : string -> string -> string val forall_of : term -> term -> term val exists_of : term -> term -> term + val type_enc_aliases : (string * string list) list val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term @@ -84,17 +84,6 @@ val default_metis_lam_trans = combsN -fun metis_call type_enc lam_trans = - let - val type_enc = - (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of - [alias] => alias - | _ => type_enc) - val opts = - [] |> type_enc <> partial_typesN ? cons type_enc - |> lam_trans <> default_metis_lam_trans ? cons lam_trans - in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end - fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s | term_name' _ = "" diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 03 19:50:38 2014 +0100 @@ -129,6 +129,17 @@ | ord => ord in {weight = weight, precedence = precedence} end +fun metis_call type_enc lam_trans = + let + val type_enc = + (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of + [alias] => alias + | _ => type_enc) + val opts = + [] |> type_enc <> partial_typesN ? cons type_enc + |> lam_trans <> default_metis_lam_trans ? cons lam_trans + in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end + exception METIS_UNPROVABLE of unit (* Main function to start Metis proof and reconstruction *) diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 03 19:50:38 2014 +0100 @@ -10,7 +10,7 @@ sig type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override - type minimize_command = Sledgehammer_Reconstructor.minimize_command + type minimize_command = Sledgehammer_Proof_Methods.minimize_command type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params @@ -33,6 +33,7 @@ open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact +open Sledgehammer_Proof_Methods open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize @@ -49,13 +50,11 @@ NONE |> fold (fn candidate => fn accum as SOME _ => accum - | NONE => if member (op =) codes candidate then SOME candidate - else NONE) - ordered_outcome_codes + | NONE => if member (op =) codes candidate then SOME candidate else NONE) + ordered_outcome_codes |> the_default unknownN -fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i - n goal = +fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = (quote name, (if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts @@ -211,88 +210,91 @@ fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts." - else case factss of - [(_, facts)] => string_of_facts facts - | _ => - factss - |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) - |> space_implode "\n\n" + else + (case factss of + [(_, facts)] => string_of_facts facts + | _ => + factss + |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) + |> space_implode "\n\n") fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode output_result i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." - else case subgoal_count state of - 0 => + else + (case subgoal_count state of + 0 => ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state))) - | n => - let - val _ = Proof.assert_backward state - val print = - if mode = Normal andalso is_none output_result then Output.urgent_message else K () - val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug) - val ctxt = Proof.context_of state - val {facts = chained, goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt - val ho_atp = exists (is_ho_atp ctxt) provers - val reserved = reserved_isar_keyword_table () - val css = clasimpset_rule_table_of ctxt - val all_facts = - nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts - concl_t - val _ = () |> not blocking ? kill_provers - val _ = case find_first (not o is_prover_supported ctxt) provers of - SOME name => error ("No such prover: " ^ name ^ ".") - | NONE => () - val _ = print "Sledgehammering..." - val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) + | n => + let + val _ = Proof.assert_backward state + val print = + if mode = Normal andalso is_none output_result then Output.urgent_message else K () + val state = state |> Proof.map_context (silence_proof_methods debug) + val ctxt = Proof.context_of state + val {facts = chained, goal, ...} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt + val ho_atp = exists (is_ho_atp ctxt) provers + val reserved = reserved_isar_keyword_table () + val css = clasimpset_rule_table_of ctxt + val all_facts = + nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts + concl_t + val _ = () |> not blocking ? kill_provers + val _ = + (case find_first (not o is_prover_supported ctxt) provers of + SOME name => error ("No such prover: " ^ name ^ ".") + | NONE => ()) + val _ = print "Sledgehammering..." + val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) - val spying_str_of_factss = - commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) + val spying_str_of_factss = + commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) - fun get_factss provers = - let - val max_max_facts = - case max_facts of - SOME n => n - | NONE => - 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers - |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) - val _ = spying spy (fn () => (state, i, "All", - "Filtering " ^ string_of_int (length all_facts) ^ " facts")); - in - all_facts - |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t - |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) - |> spy ? tap (fn factss => spying spy (fn () => - (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) - end + fun get_factss provers = + let + val max_max_facts = + (case max_facts of + SOME n => n + | NONE => + 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers + |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) + val _ = spying spy (fn () => (state, i, "All", + "Filtering " ^ string_of_int (length all_facts) ^ " facts")); + in + all_facts + |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t + |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) + |> spy ? tap (fn factss => spying spy (fn () => + (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) + end - fun launch_provers state = - let - val factss = get_factss provers - val problem = - {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = factss} - val learn = mash_learn_proof ctxt params (prop_of goal) all_facts - val launch = launch_prover params mode output_result minimize_command only learn - in - if mode = Auto_Try then - (unknownN, state) - |> fold (fn prover => fn accum as (outcome_code, _) => - if outcome_code = someN then accum - else launch problem prover) - provers - else - provers - |> (if blocking then Par_List.map else map) (launch problem #> fst) - |> max_outcome_code |> rpair state - end - in - (if blocking then launch_provers state - else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) - handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) - end - |> `(fn (outcome_code, _) => outcome_code = someN) + fun launch_provers state = + let + val factss = get_factss provers + val problem = + {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, + factss = factss} + val learn = mash_learn_proof ctxt params (prop_of goal) all_facts + val launch = launch_prover params mode output_result minimize_command only learn + in + if mode = Auto_Try then + (unknownN, state) + |> fold (fn prover => fn accum as (outcome_code, _) => + if outcome_code = someN then accum + else launch problem prover) + provers + else + provers + |> (if blocking then Par_List.map else map) (launch problem #> fst) + |> max_outcome_code |> rpair state + end + in + (if blocking then launch_provers state + else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) + handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) + end + |> `(fn (outcome_code, _) => outcome_code = someN)) end; diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 03 19:50:38 2014 +0100 @@ -96,6 +96,7 @@ ("isar_proofs", "smart"), ("compress_isar", "10"), ("try0_isar", "true"), + ("smt_proofs", "smart"), ("slice", "true"), ("minimize", "smart"), ("preplay_timeout", "2")] @@ -117,7 +118,8 @@ ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize"), - ("dont_try0_isar", "try0_isar")] + ("dont_try0_isar", "try0_isar"), + ("no_smt_proofs", "smt_proofs")] val params_not_for_minimize = ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"]; @@ -131,12 +133,12 @@ member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = - case space_explode " " s of + (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss - | _ => false + | _ => false) fun unalias_raw_param (name, value) = - case AList.lookup (op =) alias_params name of + (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then @@ -145,13 +147,14 @@ error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \ \(cf. " ^ quote name' ^ ").") | NONE => - case AList.lookup (op =) negated_alias_params name of - SOME name' => (name', case value of - ["false"] => ["true"] - | ["true"] => ["false"] - | [] => ["false"] - | _ => value) - | NONE => (name, value) + (case AList.lookup (op =) negated_alias_params name of + SOME name' => (name', + (case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value)) + | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" @@ -266,9 +269,10 @@ val type_enc = if mode = Auto_Try then NONE - else case lookup_string "type_enc" of - "smart" => NONE - | s => (type_enc_of_string Strict s; SOME s) + else + (case lookup_string "type_enc" of + "smart" => NONE + | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" @@ -284,6 +288,7 @@ val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress_isar = Real.max (1.0, lookup_real "compress_isar") val try0_isar = lookup_bool "try0_isar" + val smt_proofs = lookup_option lookup_bool "smt_proofs" val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" val timeout = lookup_time "timeout" @@ -295,8 +300,8 @@ uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params mode diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 03 19:50:38 2014 +0100 @@ -110,18 +110,18 @@ fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s | normT (TVar (z as (_, S))) = (fn ((knownT, nT), accum) => - case find_index (equal z) knownT of + (case find_index (equal z) knownT of ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) - | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))) + | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))) | normT (T as TFree _) = pair T fun norm (t $ u) = norm t ##>> norm u #>> op $ | norm (Const (s, T)) = normT T #>> curry Const s | norm (Var (z as (_, T))) = normT T #> (fn (T, (accumT, (known, n))) => - case find_index (equal z) known of + (case find_index (equal z) known of ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) - | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))) + | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))) | norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) | norm (Bound j) = pair (Bound j) @@ -138,11 +138,11 @@ Induction else let val t = normalize_vars t in - case Termtab.lookup css t of + (case Termtab.lookup css t of SOME status => status | NONE => let val concl = Logic.strip_imp_concl t in - case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of + (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of SOME lrhss => let val prems = Logic.strip_imp_prems t @@ -150,8 +150,8 @@ in Termtab.lookup css t' |> the_default General end - | NONE => General - end + | NONE => General) + end) end end @@ -165,15 +165,14 @@ map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args |> implode fun nth_name j = - case xref of + (case xref of Facts.Fact s => backquote s ^ bracket | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket | Facts.Named ((name, _), SOME intervals) => make_name reserved true - (nth (maps (explode_interval (length ths)) intervals) j) name ^ - bracket + (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) fun add_nth th (j, rest) = let val name = nth_name j in (j + 1, ((name, stature_of_thm false [] chained css name th), th) @@ -364,9 +363,9 @@ corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) fun un_class_ify s = - case first_field "_class" s of + (case first_field "_class" s of SOME (pref, suf) => [s, pref ^ suf] - | NONE => [s] + | NONE => [s]) fun build_name_tables name_of facts = let @@ -388,7 +387,7 @@ |> Net.entries fun struct_induct_rule_on th = - case Logic.strip_horn (prop_of th) of + (case Logic.strip_horn (prop_of th) of (prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => if not (is_TVar ind_T) andalso length prems > 1 andalso @@ -397,7 +396,7 @@ SOME (p_name, ind_T) else NONE - | _ => NONE + | _ => NONE) val instantiate_induct_timeout = seconds 0.01 @@ -420,14 +419,15 @@ handle Type.TYPE_MATCH => false fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = - case struct_induct_rule_on th of + (case struct_induct_rule_on th of SOME (p_name, ind_T) => let val thy = Proof_Context.theory_of ctxt in - stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) - |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout - (instantiate_induct_rule ctxt stmt p_name ax))) + stmt_xs + |> filter (fn (_, T) => type_match thy (T, ind_T)) + |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout + (instantiate_induct_rule ctxt stmt p_name ax))) end - | NONE => [ax] + | NONE => [ax]) fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) @@ -482,9 +482,9 @@ val n = length ths val multi = n > 1 fun check_thms a = - case try (Proof_Context.get_thms ctxt) a of + (case try (Proof_Context.get_thms ctxt) a of NONE => false - | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') + | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) in snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) => (j - 1, diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 19:50:38 2014 +0100 @@ -11,16 +11,16 @@ type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature - type one_line_params = Sledgehammer_Reconstructor.one_line_params + type one_line_params = Sledgehammer_Proof_Methods.one_line_params val trace : bool Config.T type isar_params = bool * (string option * string option) * Time.time * real * bool * bool - * (term, string) atp_step list * thm + * (term, string) atp_step list * thm - val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int -> - one_line_params -> string + val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) -> + int -> one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = @@ -31,7 +31,7 @@ open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress @@ -109,12 +109,13 @@ type isar_params = bool * (string option * string option) * Time.time * real * bool * bool - * (term, string) atp_step list * thm + * (term, string) atp_step list * thm val arith_methods = [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, Algebra_Method, Metis_Method (NONE, NONE), Meson_Method] -val datatype_methods = [Simp_Method, Simp_Size_Method] +val datatype_methods = + [Simp_Method, Simp_Size_Method] val metislike_methods0 = [Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method, Force_Method, Algebra_Method, Meson_Method, @@ -122,9 +123,10 @@ val rewrite_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE), Meson_Method] -val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method] +val skolem_methods = + [Metis_Method (NONE, NONE), Blast_Method, Meson_Method] -fun isar_proof_text ctxt debug isar_proofs isar_params +fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let fun isar_proof_of () = @@ -134,7 +136,10 @@ val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0 - val massage_meths = not try0_isar ? single o hd + fun massage_meths (meths as meth :: _) = + if not try0_isar then [meth] + else if smt_proofs = SOME true then SMT_Method :: meths + else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params @@ -169,7 +174,7 @@ else ([], rewrite_methods)) ||> massage_meths in - Prove ([], skos, l, t, [], ([], []), meths) + Prove ([], skos, l, t, [], ([], []), meths, "") end) val bot = atp_proof |> List.last |> #1 @@ -218,7 +223,7 @@ accum |> (if tainted = [] then cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], - (the_list predecessor, []), massage_meths metislike_methods)) + (the_list predecessor, []), massage_meths metislike_methods, "")) else I) |> rev @@ -237,7 +242,7 @@ else metislike_methods) |> massage_meths - fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths) + fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "") fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then @@ -251,7 +256,7 @@ steps_of_rest (prove [] deps) | _ => steps_of_rest (prove [] deps)) else - steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths) + steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "") else prove [] deps) end | isar_steps outer predecessor accum (Cases cases :: infs) = @@ -264,7 +269,7 @@ val step = Prove (maybe_show outer c [], [], l, t, map isar_case (filter_out (null o snd) cases), - (the_list predecessor, []), massage_meths metislike_methods) + (the_list predecessor, []), massage_meths metislike_methods, "") in isar_steps outer (SOME l) (step :: accum) infs end @@ -284,9 +289,7 @@ |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically - val ctxt = ctxt - |> enrich_context_with_local_facts canonical_isar_proof - |> silence_reconstructors debug + val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty @@ -296,7 +299,6 @@ fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" - fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) @@ -304,11 +306,17 @@ fun trace_isar_proof label proof = if trace then - tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^ - "\n") + tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ + string_of_isar_proof (comment_isar_proof comment_of proof) ^ "\n") else () + fun comment_of l (meth :: _) = + (case (verbose, + Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of + (false, Played _) => "" + | (_, outcome) => string_of_play_outcome outcome) + val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") @@ -319,11 +327,12 @@ #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) + ||> comment_isar_proof comment_of ||> chain_isar_proof ||> kill_useless_labels_in_isar_proof - ||> relabel_isar_proof_finally + ||> relabel_isar_proof_nicely in - (case string_of_isar_proof (K (K "")) isar_proof of + (case string_of_isar_proof isar_proof of "" => if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." else "" @@ -354,18 +363,18 @@ if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") in one_line_proof ^ isar_proof end -fun isar_proof_would_be_a_good_idea (reconstr, play) = +fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = (case play of - Played _ => reconstr = SMT + Played _ => meth = SMT_Method andalso smt_proofs <> SOME true | Play_Timed_Out _ => true | Play_Failed => true | Not_Played => false) -fun proof_text ctxt debug isar_proofs isar_params num_chained +fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = (if isar_proofs = SOME true orelse - (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then - isar_proof_text ctxt debug isar_proofs isar_params + (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then + isar_proof_text ctxt debug isar_proofs smt_proofs isar_params else one_line_proof_text num_chained) one_line_params diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Mon Feb 03 19:50:38 2014 +0100 @@ -41,12 +41,12 @@ post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd fun fold_map_atypes f T s = - case T of + (case T of Type (name, Ts) => - let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in - (Type (name, Ts), s) - end - | _ => f T s + let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in + (Type (name, Ts), s) + end + | _ => f T s) val indexname_ord = Term_Ord.fast_indexname_ord val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 19:50:38 2014 +0100 @@ -19,7 +19,7 @@ struct open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay @@ -32,7 +32,7 @@ | collect_steps [] accum = accum | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) and collect_step (Let _) x = x - | collect_step (step as Prove (_, _, l, _, subproofs, _, _)) x = + | collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x = (case collect_subproofs subproofs x of ([], accu) => ([], accu) | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum) @@ -55,16 +55,16 @@ | update_steps (step :: steps) updates = update_step step (update_steps steps updates) and update_step step (steps, []) = (step :: steps, []) | update_step (step as Let _) (steps, updates) = (step :: steps, updates) - | update_step (Prove (qs, xs, l, t, subproofs, facts, meths)) - (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths') :: updates') = - let - val (subproofs, updates) = - if l = l' then update_subproofs subproofs' updates' - else update_subproofs subproofs updates - in - if l = l' then (Prove (qs', xs', l', t', subproofs, facts', meths') :: steps, updates) - else (Prove (qs, xs, l, t, subproofs, facts, meths) :: steps, updates) - end + | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) + (steps, + updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') = + (if l = l' then + update_subproofs subproofs' updates' + |>> (fn subproofs' => Prove (qs', xs', l', t', subproofs', facts', meths', comment')) + else + update_subproofs subproofs updates + |>> (fn subproofs => Prove (qs, xs, l, t, subproofs, facts, meths, comment))) + |>> (fn step => step :: steps) and update_subproofs [] updates = ([], updates) | update_subproofs steps [] = (steps, []) | update_subproofs (proof :: subproofs) updates = @@ -80,18 +80,30 @@ | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") end -fun try_merge (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1)) - (Prove (qs2, fix, l2, t, subproofs, (lfs2, gfs2), meths2)) = - (case inter (op =) meths1 meths2 of +fun merge_methods preplay_data (l1, meths1) (l2, meths2) = + let + fun is_method_hopeful l meth = + let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in + not (Lazy.is_finished outcome) orelse + (case Lazy.force outcome of Played _ => true | _ => false) + end + in + inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2) + end + +fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) + (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) = + (case merge_methods preplay_data (l1, meths1) (l2, meths2) of [] => NONE | meths => let val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) val gfs = union (op =) gfs1 gfs2 in - SOME (Prove (qs2, fix, l2, t, subproofs, (lfs, gfs), meths)) + SOME (Prove (qs2, fix, l2, t, subproofs1 @ subproofs2, (lfs, gfs), meths, + comment1 ^ comment2)) end) - | try_merge _ _ = NONE + | try_merge _ _ _ = NONE val compress_degree = 2 val merge_timeout_slack_time = seconds 0.005 @@ -117,9 +129,9 @@ val (get_successors, replace_successor) = let - fun add_refs (Let _) = I - | add_refs (Prove (_, _, v, _, _, (lfs, _), _)) = - fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs + fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) = + fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs + | add_refs _ = I val tab = Canonical_Label_Tab.empty @@ -140,11 +152,11 @@ end (* elimination of trivial, one-step subproofs *) - fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs = + fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) comment subs nontriv_subs = if null subs orelse not (compress_further ()) then let val subproofs = List.revAppend (nontriv_subs, subs) - val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths) + val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment) in set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)]; step @@ -154,7 +166,7 @@ (sub as Proof (_, assms, sub_steps)) :: subs => (let (* trivial subproofs have exactly one "Prove" step *) - val [Prove (_, [], l', _, [], (lfs', gfs'), meths')] = sub_steps + val [Prove (_, [], l', _, [], (lfs', gfs'), meths', _)] = sub_steps (* only touch proofs that can be preplayed sucessfully *) val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l' @@ -163,8 +175,8 @@ val subs'' = subs @ nontriv_subs val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs') val gfs'' = union (op =) gfs' gfs - val meths'' as _ :: _ = inter (op =) meths' meths - val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'') + val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths) + val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'', comment) (* check if the modified step can be preplayed fast enough *) val timeout = slackify_merge_timeout (Time.+ (time, time')) @@ -172,20 +184,20 @@ in decrement_step_count (); (* l' successfully eliminated! *) map (replace_successor l' [l]) lfs'; - elim_one_subproof time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs + elim_one_subproof time'' qs fix l t lfs'' gfs'' meths comment subs nontriv_subs end handle Bind => - elim_one_subproof time qs fix l t lfs gfs meths subs (sub :: nontriv_subs)) + elim_one_subproof time qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs)) | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof") - fun elim_subproofs (step as Let _) = step - | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths)) = + fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) = if subproofs = [] then step else (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of - Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs [] + Played time => elim_one_subproof time qs fix l t lfs gfs meths comment subproofs [] | _ => step) + | elim_subproofs step = step fun compress_top_level steps = let @@ -198,8 +210,8 @@ val cand_ord = pairself cand_key #> compression_ord - fun pop_next_cand [] = (NONE, []) - | pop_next_cand (cands as (cand :: cands')) = + fun pop_next_candidate [] = (NONE, []) + | pop_next_candidate (cands as (cand :: cands')) = let val best as (i, _, _) = fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand @@ -207,8 +219,8 @@ val candidates = let - fun add_cand (_, Let _) = I - | add_cand (i, Prove (_, _, l, t, _, _, _)) = cons (i, l, size_of_term t) + fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t) + | add_cand _ = I in (steps |> split_last |> fst (* keep last step *) @@ -217,15 +229,16 @@ fun try_eliminate (i, l, _) labels steps = let - val ((cand as Prove (_, _, _, _, _, (lfs, _), _)) :: steps') = drop i steps + val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps val succs = collect_successors steps' labels (* only touch steps that can be preplayed successfully *) val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l - val succs' = map (try_merge cand #> the) succs + val succs' = map (try_merge (!preplay_data) cand #> the) succs + (* FIXME: more generous! *) val times0 = map ((fn Played time => time) o forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time @@ -236,16 +249,16 @@ (* ensure none of the modified successors timed out *) val times = map (fn (_, Played time) :: _ => time) meths_outcomess - val (steps1, _ :: steps2) = chop i steps + val (steps_before, _ :: steps_after) = chop i steps (* replace successors with their modified versions *) - val steps2 = update_steps steps2 succs' + val steps_after = update_steps steps_after succs' in decrement_step_count (); (* candidate successfully eliminated *) map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times succs' meths_outcomess; map (replace_successor l labels) lfs; (* removing the step would mess up the indices; replace with dummy step instead *) - steps1 @ dummy_isar_step :: steps2 + steps_before @ dummy_isar_step :: steps_after end handle Bind => steps | Match => steps @@ -255,7 +268,7 @@ if not (compress_further ()) then steps else - (case pop_next_cand candidates of + (case pop_next_candidate candidates of (NONE, _) => steps (* no more candidates for elimination *) | (SOME (cand as (_, l, _)), candidates) => let val successors = get_successors l in @@ -280,9 +293,9 @@ steps |> map (fn step => step |> compress_further () ? compress_sub_levels) |> compress_further () ? compress_top_level and compress_sub_levels (step as Let _) = step - | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths)) = + | compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = (* compress subproofs *) - Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths) + Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment) (* eliminate trivial subproofs *) |> compress_further () ? elim_subproofs in diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 19:50:38 2014 +0100 @@ -21,22 +21,25 @@ structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = struct -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay -fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) = - Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l]) +fun keep_fastest_method_of_isar_step preplay_data + (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = + Prove (qs, xs, l, t, subproofs, facts, + meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, + comment) | keep_fastest_method_of_isar_step _ step = step val slack = seconds 0.1 fun minimize_isar_step_dependencies ctxt preplay_data - (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) = + (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => let - fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths) + fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment) fun minimize_facts _ time min_facts [] = (time, min_facts) | minimize_facts mk_step time min_facts (f :: facts) = @@ -75,7 +78,7 @@ else (used, accu)) and process_used_step step = step |> postproc_step |> process_used_step_subproofs - and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) = + and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = let val (used, subproofs) = map process_proof subproofs @@ -83,7 +86,7 @@ |>> Ord_List.unions label_ord |>> fold (Ord_List.insert label_ord) lfs in - (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) + (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) end in snd o process_proof diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 19:50:38 2014 +0100 @@ -7,7 +7,7 @@ signature SLEDGEHAMMER_ISAR_PREPLAY = sig - type play_outcome = Sledgehammer_Reconstructor.play_outcome + type play_outcome = Sledgehammer_Proof_Methods.play_outcome type proof_method = Sledgehammer_Isar_Proof.proof_method type isar_step = Sledgehammer_Isar_Proof.isar_step type isar_proof = Sledgehammer_Isar_Proof.isar_proof @@ -36,7 +36,7 @@ open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) @@ -52,9 +52,9 @@ fun enrich_with_proof (Proof (_, assms, isar_steps)) = enrich_with_assms assms #> fold enrich_with_step isar_steps - and enrich_with_step (Let _) = I - | enrich_with_step (Prove (_, _, l, t, subproofs, _, _)) = + and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) = enrich_with_fact l t #> fold enrich_with_proof subproofs + | enrich_with_step _ = I in enrich_with_proof proof ctxt end @@ -88,7 +88,7 @@ val concl = (case try List.last steps of - SOME (Prove (_, [], _, t, _, _, _)) => t + SOME (Prove (_, [], _, t, _, _, _, _)) => t | _ => raise Fail "preplay error: malformed subproof") val var_idx = maxidx_of_term concl + 1 @@ -100,29 +100,8 @@ |> Skip_Proof.make_thm thy end -fun tac_of_method ctxt (local_facts, global_facts) meth = - Method.insert_tac local_facts THEN' - (case meth of - Meson_Method => Meson.meson_tac ctxt global_facts - | Metis_Method (type_enc_opt, lam_trans_opt) => - Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] - (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts - | _ => - Method.insert_tac global_facts THEN' - (case meth of - Simp_Method => Simplifier.asm_full_simp_tac ctxt - | Simp_Size_Method => - Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) - | Auto_Method => K (Clasimp.auto_tac ctxt) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Arith_Method => Arith_Data.arith_tac ctxt - | Blast_Method => blast_tac ctxt - | Algebra_Method => Groebner.algebra_tac [] [] ctxt - | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method")) - -(* main function for preplaying Isar steps; may throw exceptions *) -fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) = +(* may throw exceptions *) +fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) = let val goal = (case xs of @@ -131,10 +110,10 @@ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis (cf. "~~/src/Pure/Isar/obtain.ML") *) let - (* FIXME: generate fresh name *) - val thesis = Free ("thesis_preplay", HOLogic.boolT) + val frees = map Free xs + val thesis = + Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) val thesis_prop = HOLogic.mk_Trueprop thesis - val frees = map Free xs (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *) val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) @@ -143,18 +122,18 @@ Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) end) - val facts = - resolve_fact_names ctxt fact_names + val assmsp = + resolve_fact_names ctxt facts |>> append (map (thm_of_proof ctxt) subproofs) fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => - HEADGOAL (tac_of_method ctxt facts meth)) + HEADGOAL (tac_of_proof_method ctxt assmsp meth)) handle ERROR msg => error ("Preplay error: " ^ msg) val play_outcome = take_time timeout prove () in - (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); + (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); play_outcome) end @@ -185,7 +164,7 @@ Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data - (step as Prove (_, _, l, _, _, _, meths)) meths_outcomes0 = + (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = let fun lazy_preplay meth = Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step) @@ -228,8 +207,8 @@ #> get_best_method_outcome Lazy.force #> fst -fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) = - Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths)) +fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) = + Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths)) | forced_outcome_of_step _ _ = Played Time.zeroTime fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 19:50:38 2014 +0100 @@ -8,37 +8,25 @@ signature SLEDGEHAMMER_ISAR_PROOF = sig + type proof_method = Sledgehammer_Proof_Methods.proof_method + type label = string * int type facts = label list * string list (* local and global facts *) datatype isar_qualifier = Show | Then - datatype proof_method = - Metis_Method of string option * string option | - Simp_Method | - Simp_Size_Method | - Auto_Method | - Fastforce_Method | - Force_Method | - Arith_Method | - Blast_Method | - Meson_Method | - Algebra_Method - datatype isar_proof = Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = Let of term * term | Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list - * facts * proof_method list + * facts * proof_method list * string val no_label : label val label_ord : label * label -> order val string_of_label : label -> string - val string_of_proof_method : proof_method -> string - val steps_of_isar_proof : isar_proof -> isar_step list val label_of_isar_step : isar_step -> label option @@ -53,13 +41,13 @@ val canonical_label_ord : (label * label) -> order + val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof val chain_isar_proof : isar_proof -> isar_proof val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof val relabel_isar_proof_canonically : isar_proof -> isar_proof - val relabel_isar_proof_finally : isar_proof -> isar_proof + val relabel_isar_proof_nicely : isar_proof -> isar_proof - val string_of_isar_proof : Proof.context -> int -> int -> - (label -> proof_method list -> string) -> isar_proof -> string + val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string end; structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = @@ -70,7 +58,7 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Annotate type label = string * int @@ -78,24 +66,12 @@ datatype isar_qualifier = Show | Then -datatype proof_method = - Metis_Method of string option * string option | - Simp_Method | - Simp_Size_Method | - Auto_Method | - Fastforce_Method | - Force_Method | - Arith_Method | - Blast_Method | - Meson_Method | - Algebra_Method - datatype isar_proof = Proof of (string * typ) list * (label * term) list * isar_step list and isar_step = Let of term * term | Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list - * facts * proof_method list + * facts * proof_method list * string val no_label = ("", ~1) @@ -103,33 +79,18 @@ fun string_of_label (s, num) = s ^ string_of_int num -fun string_of_proof_method meth = - (case meth of - Metis_Method (NONE, NONE) => "metis" - | Metis_Method (type_enc_opt, lam_trans_opt) => - "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" - | Simp_Method => "simp" - | Simp_Size_Method => "simp add: size_ne_size_imp_ne" - | Auto_Method => "auto" - | Fastforce_Method => "fastforce" - | Force_Method => "force" - | Arith_Method => "arith" - | Blast_Method => "blast" - | Meson_Method => "meson" - | Algebra_Method => "algebra") - fun steps_of_isar_proof (Proof (_, _, steps)) = steps -fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l +fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l | label_of_isar_step _ = NONE -fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _)) = subs +fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs | subproofs_of_isar_step _ = [] -fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _)) = facts +fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts | facts_of_isar_step _ = ([], []) -fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths)) = meths +fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths | proof_methods_of_isar_step _ = [] fun fold_isar_step f step = @@ -140,8 +101,8 @@ let fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps) and map_step (step as Let _) = f step - | map_step (Prove (qs, xs, l, t, subs, facts, meths)) = - f (Prove (qs, xs, l, t, map map_proof subs, facts, meths)) + | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = + f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment)) in map_proof end val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) @@ -153,12 +114,17 @@ type key = label val ord = canonical_label_ord) +fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) = + Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths) + | comment_isar_step _ step = step +fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of) + fun chain_qs_lfs NONE lfs = ([], lfs) | chain_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs) -fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) = +fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) = let val (qs', lfs) = chain_qs_lfs lbl lfs in - Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths) + Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment) end | chain_isar_step _ step = step and chain_isar_steps _ [] = [] @@ -175,8 +141,8 @@ fun kill_label l = if member (op =) used_ls l then l else no_label - fun kill_step (Prove (qs, xs, l, t, subs, facts, meths)) = - Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths) + fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = + Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment) | kill_step step = step and kill_proof (Proof (fix, assms, steps)) = Proof (fix, map (apfst kill_label) assms, map kill_step steps) @@ -189,14 +155,15 @@ fun next_label l (next, subst) = let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end - fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) = + fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment)) + (accum as (_, subst)) = let val lfs' = maps (the_list o AList.lookup (op =) subst) lfs val ((subs', l'), accum') = accum |> fold_map relabel_proof subs ||>> next_label l in - (Prove (qs, fix, l', t, subs', (lfs', gfs), meths), accum') + (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum') end | relabel_step step accum = (step, accum) and relabel_proof (Proof (fix, assms, steps)) = @@ -210,7 +177,7 @@ val assume_prefix = "a" val have_prefix = "f" -val relabel_isar_proof_finally = +val relabel_isar_proof_nicely = let fun next_label depth prefix l (accum as (next, subst)) = if l = no_label then @@ -220,13 +187,14 @@ (l', (next + 1, (l, l') :: subst)) end - fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths)) (accum as (_, subst)) = + fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) + (accum as (_, subst)) = let val lfs' = maps (the_list o AList.lookup (op =) subst) lfs val (l', accum' as (next', subst')) = next_label depth have_prefix l accum val subs' = map (relabel_proof subst' (depth + 1)) subs in - (Prove (qs, xs, l', t, subs', (lfs', gfs), meths), accum') + (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum') end | relabel_step _ step accum = (step, accum) and relabel_proof subst depth (Proof (fix, assms, steps)) = @@ -240,7 +208,7 @@ val indent_size = 2 -fun string_of_isar_proof ctxt i n comment_of proof = +fun string_of_isar_proof ctxt i n proof = let (* Make sure only type constraints inserted by the type annotation code are printed. *) val ctxt = @@ -291,6 +259,7 @@ fun is_direct_method (Metis_Method _) = true | is_direct_method Meson_Method = true + | is_direct_method SMT_Method = true | is_direct_method _ = false (* Local facts are always passed via "using", which affects "meson" and "metis". This is @@ -336,7 +305,7 @@ and add_step ind (Let (t1, t2)) = add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n" - | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _)) = + | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _, comment)) = add_step_pre ind qs subs #> (case xs of [] => add_str (of_have qs (length subs) ^ " ") @@ -345,9 +314,7 @@ #> add_term t #> add_str (" " ^ of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ - (case comment_of l meths of - "" => "" - | comment => " (* " ^ comment ^ " *)") ^ "\n") + (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") and add_steps ind = fold (add_step ind) and of_proof ind ctxt (Proof (xs, assms, steps)) = ("", ctxt) @@ -359,7 +326,7 @@ (* One-step Metis proofs are pointless; better use the one-liner directly. *) (case proof of Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *) - | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _)]) => "" + | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => "" | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 03 19:50:38 2014 +0100 @@ -178,9 +178,9 @@ fun run_on () = (Isabelle_System.bash command |> tap (fn _ => - case try File.read (Path.explode err_file) |> the_default "" of + (case try File.read (Path.explode err_file) |> the_default "" of "" => trace_msg ctxt (K "Done") - | s => warning ("MaSh error: " ^ elide_string 1000 s)); + | s => warning ("MaSh error: " ^ elide_string 1000 s))); read_suggs (fn () => try File.read_lines sugg_path |> these)) fun clean_up () = if overlord then () @@ -243,17 +243,16 @@ (* The suggested weights don't make much sense. *) fun extract_suggestion sugg = - case space_explode "=" sugg of + (case space_explode "=" sugg of [name, _ (* weight *)] => SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *)) | [name] => SOME (unencode_str name (* , 1.0 *)) - | _ => NONE + | _ => NONE) fun extract_suggestions line = - case space_explode ":" line of - [goal, suggs] => - (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) - | _ => ("", []) + (case space_explode ":" line of + [goal, suggs] => (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs)) + | _ => ("", [])) structure MaSh = struct @@ -294,11 +293,10 @@ fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); - run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) - (fn suggs => - case suggs () of - [] => [] - | suggs => snd (extract_suggestions (List.last suggs))) + run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs => + (case suggs () of + [] => [] + | suggs => snd (extract_suggestions (List.last suggs)))) handle List.Empty => []) end; @@ -362,48 +360,47 @@ exception FILE_VERSION_TOO_NEW of unit fun extract_node line = - case space_explode ":" line of + (case space_explode ":" line of [head, parents] => (case space_explode " " head of - [kind, name] => - SOME (unencode_str name, unencode_strs parents, - try proof_kind_of_str kind |> the_default Isar_Proof) - | _ => NONE) - | _ => NONE + [kind, name] => + SOME (unencode_str name, unencode_strs parents, + try proof_kind_of_str kind |> the_default Isar_Proof) + | _ => NONE) + | _ => NONE) fun load_state _ _ (state as (true, _)) = state | load_state ctxt overlord _ = let val path = mash_state_file () in (true, - case try File.read_lines path of + (case try File.read_lines path of SOME (version' :: node_lines) => let fun add_edge_to name parent = Graph.default_node (parent, Isar_Proof) #> Graph.add_edge (parent, name) fun add_node line = - case extract_node line of + (case extract_node line of NONE => I (* shouldn't happen *) | SOME (name, parents, kind) => - update_access_graph_node (name, kind) - #> fold (add_edge_to name) parents + update_access_graph_node (name, kind) #> fold (add_edge_to name) parents) val (access_G, num_known_facts) = - case string_ord (version', version) of + (case string_ord (version', version) of EQUAL => (try_graph ctxt "loading state" Graph.empty (fn () => - fold add_node node_lines Graph.empty), + fold add_node node_lines Graph.empty), length node_lines) | LESS => (* can't parse old file *) (MaSh.unlearn ctxt overlord; (Graph.empty, 0)) - | GREATER => raise FILE_VERSION_TOO_NEW () + | GREATER => raise FILE_VERSION_TOO_NEW ()) in trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")"); {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []} end - | _ => empty_state) + | _ => empty_state)) end fun save_state _ (state as {dirty = SOME [], ...}) = state @@ -415,10 +412,9 @@ fun append_entry (name, (kind, (parents, _))) = cons (name, Graph.Keys.dest parents, kind) val (banner, entries) = - case dirty of - SOME names => - (NONE, fold (append_entry o Graph.get_entry access_G) names []) - | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []) + (case dirty of + SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names []) + | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])) in write_file banner (entries, str_of_entry) (mash_state_file ()); trace_msg ctxt (fn () => @@ -471,11 +467,11 @@ if Thm.has_name_hint th then let val hint = Thm.get_name_hint th in (* There must be a better way to detect local facts. *) - case try (unprefix local_prefix) hint of + (case try (unprefix local_prefix) hint of SOME suf => - thy_name_of_thm th ^ Long_Name.separator ^ suf ^ - Long_Name.separator ^ elided_backquote_thm 50 th - | NONE => hint + thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^ + elided_backquote_thm 50 th + | NONE => hint) end else elided_backquote_thm 200 th @@ -512,9 +508,9 @@ let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in - case find_index (curry fact_eq fact o fst) sels of + (case find_index (curry fact_eq fact o fst) sels of ~1 => if member fact_eq unks fact then NONE else SOME 0.0 - | rank => score_at rank + | rank => score_at rank) end fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] @@ -536,20 +532,21 @@ if Theory.eq_thy p then EQUAL else LESS else if Theory.subthy (swap p) then GREATER - else case int_ord (pairself (length o Theory.ancestors_of) p) of - EQUAL => string_ord (pairself Context.theory_name p) - | order => order + else + (case int_ord (pairself (length o Theory.ancestors_of) p) of + EQUAL => string_ord (pairself Context.theory_name p) + | order => order) fun crude_thm_ord p = - case crude_theory_ord (pairself theory_of_thm p) of + (case crude_theory_ord (pairself theory_of_thm p) of EQUAL => let val q = pairself nickname_of_thm p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) - case bool_ord (pairself (String.isSuffix "_def") (swap q)) of + (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q - | ord => ord + | ord => ord) end - | ord => ord + | ord => ord) val thm_less_eq = Theory.subthy o pairself theory_of_thm fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) @@ -724,7 +721,7 @@ add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t fun add_term Ts = add_term_pats Ts term_max_depth fun add_subterms Ts t = - case strip_comb t of + (case strip_comb t of (Const (s, T), args) => (not (is_widely_irrelevant_const s) ? add_term Ts t) #> add_subtypes T @@ -735,7 +732,7 @@ | Var (_, T) => add_subtypes T | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body | _ => I) - #> fold (add_subterms Ts) args + #> fold (add_subterms Ts) args) in [] |> fold (add_subterms []) ts end val term_max_depth = 2 @@ -805,7 +802,7 @@ fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts name_tabs th = - case isar_dependencies_of name_tabs th of + (case isar_dependencies_of name_tabs th of [] => (false, []) | isar_deps => let @@ -819,9 +816,10 @@ fun add_isar_dep facts dep accum = if exists (is_dep dep) accum then accum - else case find_first (is_dep dep) facts of - SOME ((_, status), th) => accum @ [(("", status), th)] - | NONE => accum (* shouldn't happen *) + else + (case find_first (is_dep dep) facts of + SOME ((_, status), th) => accum @ [(("", status), th)] + | NONE => accum (* shouldn't happen *)) val mepo_facts = facts |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE @@ -838,7 +836,7 @@ |> Output.urgent_message else (); - case run_prover_for_mash ctxt params prover name facts goal of + (case run_prover_for_mash ctxt params prover name facts goal of {outcome = NONE, used_facts, ...} => (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in @@ -849,8 +847,8 @@ else (); (true, map fst used_facts)) - | _ => (false, isar_deps) - end + | _ => (false, isar_deps)) + end) (*** High-level communication with MaSh ***) @@ -1140,9 +1138,9 @@ val access_G = access_G |> fold flop_wrt_access_graph flops val num_known_facts = num_known_facts + length learns val dirty = - case (was_empty, dirty, relearns) of + (case (was_empty, dirty, relearns) of (false, SOME names, []) => SOME (map #1 learns @ names) - | _ => NONE + | _ => NONE) in MaSh.learn ctxt overlord (save andalso null relearns) (rev learns); MaSh.relearn ctxt overlord save relearns; @@ -1202,9 +1200,9 @@ let val name = nickname_of_thm th val (n, relearns, flops) = - case deps_of status th of + (case deps_of status th of SOME deps => (n + 1, (name, deps) :: relearns, flops) - | NONE => (n, relearns, name :: flops) + | NONE => (n, relearns, name :: flops)) val (relearns, flops, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then (commit false [] relearns flops; @@ -1325,7 +1323,7 @@ in if length facts - num_known_facts <= max_facts_to_learn_before_query then - case length (filter_out is_in_access_G facts) of + (case length (filter_out is_in_access_G facts) of 0 => false | num_facts_to_learn => if num_facts_to_learn <= max_facts_to_learn_before_query then @@ -1333,21 +1331,21 @@ |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s)); true) else - (maybe_launch_thread (); false) + (maybe_launch_thread (); false)) else (maybe_launch_thread (); false) end else false val (save, effective_fact_filter) = - case fact_filter of + (case fact_filter of SOME ff => (ff <> mepoN andalso maybe_learn (), ff) | NONE => if is_mash_enabled () then (maybe_learn (), if mash_can_suggest_facts ctxt overlord then meshN else mepoN) else - (false, mepoN) + (false, mepoN)) val unique_facts = drop_duplicate_facts facts val add_ths = Attrib.eval_thms ctxt add @@ -1373,11 +1371,11 @@ val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take in if save then MaSh.save ctxt overlord else (); - case (fact_filter, mess) of + (case (fact_filter, mess) of (NONE, [(_, (mepo, _)), (_, (mash, _))]) => [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take), (mashN, mash |> map fst |> add_and_take)] - | _ => [(effective_fact_filter, mesh)] + | _ => [(effective_fact_filter, mesh)]) end fun kill_learners ctxt ({overlord, ...} : params) = diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Mon Feb 03 19:50:38 2014 +0100 @@ -171,7 +171,7 @@ (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x)) #> fold (do_term false) ts and do_term ext_arg t = - case strip_comb t of + (case strip_comb t of (Const x, ts) => do_const true x ts | (Free x, ts) => do_const false x ts | (Abs (_, T, t'), ts) => @@ -182,11 +182,11 @@ ? add_pconst_to_table (pseudo_abs_name, PType (order_of_type T + 1, []))) #> fold (do_term false) (t' :: ts) - | (_, ts) => fold (do_term false) ts + | (_, ts) => fold (do_term false) ts) and do_term_or_formula ext_arg T = if T = HOLogic.boolT then do_formula else do_term ext_arg and do_formula t = - case t of + (case t of Const (@{const_name all}, _) $ Abs (_, _, t') => do_formula t' | @{const "==>"} $ t1 $ t2 => do_formula t1 #> do_formula t2 | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => @@ -212,7 +212,7 @@ do_formula (t1 $ Bound ~1) #> do_formula t' | (t0 as Const (_, @{typ bool})) $ t1 => do_term false t0 #> do_formula t1 (* theory constant *) - | _ => do_term false t + | _ => do_term false t) in do_formula end fun pconsts_in_fact thy t = @@ -233,17 +233,16 @@ theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) fun pair_consts_fact thy fudge fact = - case fact |> snd |> theory_const_prop_of fudge - |> pconsts_in_fact thy of + (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of [] => NONE - | consts => SOME ((fact, consts), NONE) + | consts => SOME ((fact, consts), NONE)) (* A two-dimensional symbol table counts frequencies of constants. It's keyed first by constant name and second by its list of type instantiations. For the latter, we need a linear ordering on "pattern list". *) fun patternT_ord p = - case p of + (case p of (Type (s, ps), Type (t, qs)) => (case fast_string_ord (s, t) of EQUAL => dict_ord patternT_ord (ps, qs) @@ -253,7 +252,7 @@ | (Type _, TVar _) => GREATER | (Type _, TFree _) => LESS | (TFree (s, _), TFree (t, _)) => fast_string_ord (s, t) - | (TFree _, _) => GREATER + | (TFree _, _) => GREATER) fun ptype_ord (PType (m, ps), PType (n, qs)) = (case dict_ord patternT_ord (ps, qs) of EQUAL => int_ord (m, n) @@ -269,11 +268,11 @@ |> Symtab.map_default (s, PType_Tab.empty) #> fold do_term ts and do_term t = - case strip_comb t of + (case strip_comb t of (Const x, ts) => do_const true x ts | (Free x, ts) => do_const false x ts | (Abs (_, _, t'), ts) => fold do_term (t' :: ts) - | (_, ts) => fold do_term ts + | (_, ts) => fold do_term ts) in do_term o theory_const_prop_of fudge o snd end fun pow_int _ 0 = 1.0 @@ -356,7 +355,7 @@ fun fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts = - case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab) + (case fact_consts |> List.partition (pconst_hyper_mem I rel_const_tab) ||> filter_out (pconst_hyper_mem swap rel_const_tab) of ([], _) => 0.0 | (rel, irrel) => @@ -373,7 +372,7 @@ o irrel_pconst_weight fudge const_tab chained_const_tab) irrel val res = rel_weight / (rel_weight + irrel_weight) - in if Real.isFinite res then res else 0.0 end + in if Real.isFinite res then res else 0.0 end) fun take_most_relevant ctxt max_facts remaining_max ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) @@ -411,15 +410,16 @@ let fun aux _ _ NONE = NONE | aux t args (SOME tab) = - case t of + (case t of t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 [] | Const (s, _) => (if is_widely_irrelevant_const s then SOME tab - else case Symtab.lookup tab s of - NONE => SOME (Symtab.update (s, length args) tab) - | SOME n => if n = length args then SOME tab else NONE) - | _ => SOME tab + else + (case Symtab.lookup tab s of + NONE => SOME (Symtab.update (s, length args) tab) + | SOME n => if n = length args then SOME tab else NONE)) + | _ => SOME tab) in aux (prop_of th) [] end (* FIXME: This is currently only useful for polymorphic type encodings. *) @@ -507,11 +507,10 @@ :: hopeful) = let val weight = - case cached_weight of + (case cached_weight of SOME w => w | NONE => - fact_weight fudge stature const_tab rel_const_tab - chained_const_tab fact_consts + fact_weight fudge stature const_tab rel_const_tab chained_const_tab fact_consts) in if weight >= thres then relevant ((ax, weight) :: candidates) rejects hopeful diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 03 19:50:38 2014 +0100 @@ -0,0 +1,201 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Steffen Juilf Smolka, TU Muenchen + +Reconstructors. +*) + +signature SLEDGEHAMMER_PROOF_METHODS = +sig + type stature = ATP_Problem_Generate.stature + + datatype proof_method = + Metis_Method of string option * string option | + Meson_Method | + SMT_Method | + Simp_Method | + Simp_Size_Method | + Auto_Method | + Fastforce_Method | + Force_Method | + Arith_Method | + Blast_Method | + Algebra_Method + + datatype play_outcome = + Played of Time.time | + Play_Timed_Out of Time.time | + Play_Failed | + Not_Played + + type minimize_command = string list -> string + type one_line_params = + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int + + val smtN : string + + val string_of_proof_method : proof_method -> string + val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic + val string_of_play_outcome : play_outcome -> string + val play_outcome_ord : play_outcome * play_outcome -> order + val one_line_proof_text : int -> one_line_params -> string + val silence_proof_methods : bool -> Proof.context -> Proof.context +end; + +structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = +struct + +open ATP_Util +open ATP_Problem_Generate +open ATP_Proof_Reconstruct + +datatype proof_method = + Metis_Method of string option * string option | + Meson_Method | + SMT_Method | + Simp_Method | + Simp_Size_Method | + Auto_Method | + Fastforce_Method | + Force_Method | + Arith_Method | + Blast_Method | + Algebra_Method + +datatype play_outcome = + Played of Time.time | + Play_Timed_Out of Time.time | + Play_Failed | + Not_Played + +type minimize_command = string list -> string +type one_line_params = + (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int + +val smtN = "smt" + +fun string_of_proof_method meth = + (case meth of + Metis_Method (NONE, NONE) => "metis" + | Metis_Method (type_enc_opt, lam_trans_opt) => + "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" + | Meson_Method => "meson" + | SMT_Method => "smt" + | Simp_Method => "simp" + | Simp_Size_Method => "simp add: size_ne_size_imp_ne" + | Auto_Method => "auto" + | Fastforce_Method => "fastforce" + | Force_Method => "force" + | Arith_Method => "arith" + | Blast_Method => "blast" + | Algebra_Method => "algebra") + +fun tac_of_proof_method ctxt (local_facts, global_facts) meth = + Method.insert_tac local_facts THEN' + (case meth of + Metis_Method (type_enc_opt, lam_trans_opt) => + Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] + (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts + | SMT_Method => SMT_Solver.smt_tac ctxt global_facts + | Meson_Method => Meson.meson_tac ctxt global_facts + | _ => + Method.insert_tac global_facts THEN' + (case meth of + Simp_Method => Simplifier.asm_full_simp_tac ctxt + | Simp_Size_Method => + Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) + | Auto_Method => K (Clasimp.auto_tac ctxt) + | Fastforce_Method => Clasimp.fast_force_tac ctxt + | Force_Method => Clasimp.force_tac ctxt + | Arith_Method => Arith_Data.arith_tac ctxt + | Blast_Method => blast_tac ctxt + | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) + +fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) + | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" + | string_of_play_outcome Play_Failed = "failed" + | string_of_play_outcome _ = "unknown" + +fun play_outcome_ord (Played time1, Played time2) = + int_ord (pairself Time.toMilliseconds (time1, time2)) + | play_outcome_ord (Played _, _) = LESS + | play_outcome_ord (_, Played _) = GREATER + | play_outcome_ord (Not_Played, Not_Played) = EQUAL + | play_outcome_ord (Not_Played, _) = LESS + | play_outcome_ord (_, Not_Played) = GREATER + | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = + int_ord (pairself Time.toMilliseconds (time1, time2)) + | play_outcome_ord (Play_Timed_Out _, _) = LESS + | play_outcome_ord (_, Play_Timed_Out _) = GREATER + | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL + +(* FIXME: Various bugs, esp. with "unfolding" +fun unusing_chained_facts _ 0 = "" + | unusing_chained_facts used_chaineds num_chained = + if length used_chaineds = num_chained then "" + else if null used_chaineds then "(* using no facts *) " + else "(* using only " ^ space_implode " " used_chaineds ^ " *) " +*) + +fun apply_on_subgoal _ 1 = "by " + | apply_on_subgoal 1 _ = "apply " + | apply_on_subgoal i n = + "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n + +fun command_call name [] = + name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" + | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" + +(* FIXME *) +fun proof_method_command meth i n used_chaineds num_chained ss = + (* unusing_chained_facts used_chaineds num_chained ^ *) + apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss + +fun show_time NONE = "" + | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" + +fun try_command_line banner time command = + banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "." + +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + (case minimize_command ss of + "" => "" + | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".") + +fun split_used_facts facts = + facts + |> List.partition (fn (_, (sc, _)) => sc = Chained) + |> pairself (sort_distinct (string_ord o pairself fst)) + +fun one_line_proof_text num_chained + ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = + let + val (chained, extra) = split_used_facts used_facts + + val (failed, ext_time) = + (case play of + Played time => (false, (SOME (false, time))) + | Play_Timed_Out time => (false, SOME (true, time)) + | Play_Failed => (true, NONE) + | Not_Played => (false, NONE)) + + val try_line = + map fst extra + |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained + |> (if failed then + enclose "One-line proof reconstruction failed: " + ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)" + else + try_command_line banner ext_time) + in + try_line ^ minimize_line minimize_command (map fst (extra @ chained)) + end + +(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound + exceeded" warnings and the like. *) +fun silence_proof_methods debug = + Try0.silence_methods debug + #> Config.put SMT_Config.verbose debug + +end; diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 19:50:38 2014 +0100 @@ -12,9 +12,9 @@ type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact - type reconstructor = Sledgehammer_Reconstructor.reconstructor - type play_outcome = Sledgehammer_Reconstructor.play_outcome - type minimize_command = Sledgehammer_Reconstructor.minimize_command + type proof_method = Sledgehammer_Proof_Methods.proof_method + type play_outcome = Sledgehammer_Proof_Methods.play_outcome + type minimize_command = Sledgehammer_Proof_Methods.minimize_command datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize @@ -38,6 +38,7 @@ isar_proofs : bool option, compress_isar : real, try0_isar : bool, + smt_proofs : bool option, slice : bool, minimize : bool option, timeout : Time.time, @@ -57,8 +58,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : (reconstructor * play_outcome) Lazy.lazy, - message : reconstructor * play_outcome -> string, + preplay : (proof_method * play_outcome) Lazy.lazy, + message : proof_method * play_outcome -> string, message_tail : string} type prover = @@ -66,23 +67,22 @@ -> prover_problem -> prover_result val SledgehammerN : string - val plain_metis : reconstructor val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string - val extract_reconstructor : params -> reconstructor -> string * (string * string list) list - val is_reconstructor : string -> bool + val extract_proof_method : params -> proof_method -> string * (string * string list) list + val is_proof_method : string -> bool val is_atp : theory -> string -> bool - val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list + val bunch_of_proof_methods : bool -> bool -> string -> proof_method list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list -> - Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome + Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome val remotify_atp_if_not_installed : theory -> string -> string option val isar_supported_prover_of : theory -> string -> string val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) -> - string -> reconstructor * play_outcome -> 'a + string -> proof_method * play_outcome -> 'a val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context @@ -102,7 +102,7 @@ open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Fact -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize @@ -110,9 +110,8 @@ "Async_Manager". *) val SledgehammerN = "Sledgehammer" -val reconstructor_names = [metisN, smtN] -val plain_metis = Metis (hd partial_type_encs, combsN) -val is_reconstructor = member (op =) reconstructor_names +val proof_method_names = [metisN, smtN] +val is_proof_method = member (op =) proof_method_names val is_atp = member (op =) o supported_atps @@ -148,6 +147,7 @@ isar_proofs : bool option, compress_isar : real, try0_isar : bool, + smt_proofs : bool option, slice : bool, minimize : bool option, timeout : Time.time, @@ -167,8 +167,8 @@ used_facts : (string * stature) list, used_from : fact list, run_time : Time.time, - preplay : (reconstructor * play_outcome) Lazy.lazy, - message : reconstructor * play_outcome -> string, + preplay : (proof_method * play_outcome) Lazy.lazy, + message : proof_method * play_outcome -> string, message_tail : string} type prover = @@ -183,29 +183,28 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this") -fun bunch_of_reconstructors needs_full_types lam_trans = - if needs_full_types then - [Metis (full_type_enc, lam_trans false), - Metis (really_full_type_enc, lam_trans false), - Metis (full_type_enc, lam_trans true), - Metis (really_full_type_enc, lam_trans true), - SMT] - else - [Metis (partial_type_enc, lam_trans false), - Metis (full_type_enc, lam_trans false), - Metis (no_typesN, lam_trans true), - Metis (really_full_type_enc, lam_trans true), - SMT] +fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans = + [Metis_Method (SOME full_type_enc, NONE)] @ + (if needs_full_types then + [Metis_Method (SOME full_type_enc, NONE), + Metis_Method (SOME really_full_type_enc, NONE), + Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)] + else + [Metis_Method (NONE, NONE), + Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @ + [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @ + (if smt_proofs then [SMT_Method] else []) -fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) = +fun extract_proof_method ({type_enc, lam_trans, ...} : params) + (Metis_Method (type_enc', lam_trans')) = let val override_params = - (if is_none type_enc andalso type_enc' = hd partial_type_encs then [] - else [("type_enc", [hd (unalias_type_enc type_enc')])]) @ - (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then [] - else [("lam_trans", [lam_trans'])]) + (if is_none type_enc' andalso is_none type_enc then [] + else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @ + (if is_none lam_trans' andalso is_none lam_trans then [] + else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])]) in (metisN, override_params) end - | extract_reconstructor _ SMT = (smtN, []) + | extract_proof_method _ SMT_Method = (smtN, []) (* based on "Mirabelle.can_apply" and generalized *) fun timed_apply timeout tac state i = @@ -216,49 +215,43 @@ TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end -fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans - | tac_of_reconstructor SMT = SMT_Solver.smt_tac - -fun timed_reconstructor reconstr debug timeout ths = - timed_apply timeout (silence_reconstructors debug - #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths)) +fun timed_proof_method meth timeout ths = + timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false)) -fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs = +fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) = let - fun get_preferred reconstrs = - if member (op =) reconstrs preferred then preferred - else List.last reconstrs + fun get_preferred meths = if member (op =) meths preferred then preferred else meth in if timeout = Time.zeroTime then - (get_preferred reconstrs, Not_Played) + (get_preferred meths, Not_Played) else let val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else () val ths = pairs |> sort_wrt (fst o fst) |> map snd - fun play [] [] = (get_preferred reconstrs, Play_Failed) + fun play [] [] = (get_preferred meths, Play_Failed) | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout) - | play timed_out (reconstr :: reconstrs) = + | play timed_out (meth :: meths) = let val _ = if verbose then - Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^ + Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^ "\" for " ^ string_of_time timeout ^ "...") else () val timer = Timer.startRealTimer () in - case timed_reconstructor reconstr debug timeout ths state i of - SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer)) - | _ => play timed_out reconstrs + (case timed_proof_method meth timeout ths state i of + SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer)) + | _ => play timed_out meths) end - handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs + handle TimeLimit.TimeOut => play (meth :: timed_out) meths in - play [] reconstrs + play [] meths end end @@ -275,9 +268,8 @@ val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy val (min_name, override_params) = (case preplay of - (reconstr, Played _) => - if isar_proofs = SOME true then (maybe_isar_name, []) - else extract_reconstructor params reconstr + (meth, Played _) => + if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth | _ => (maybe_isar_name, [])) in minimize_command override_params min_name end @@ -293,7 +285,7 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = - reconstructor_names @ + proof_method_names @ sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 19:50:38 2014 +0100 @@ -31,7 +31,7 @@ open ATP_Proof_Reconstruct open ATP_Systems open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_Prover @@ -132,7 +132,7 @@ fun run_atp mode name (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar, - try0_isar, slice, minimize, timeout, preplay_timeout, ...}) + try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...}) minimize_command ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -346,18 +346,15 @@ let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof - val reconstrs = - bunch_of_reconstructors needs_full_types (fn desperate => - if desperate then - if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN - else - default_metis_lam_trans) + val meths = + bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types + (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN) in (used_facts, Lazy.lazy (fn () => let val used_pairs = used_from |> filter_used_facts false used_facts in play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal - (hd reconstrs) reconstrs + (hd meths) meths end), fn preplay => let @@ -383,7 +380,7 @@ subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt debug isar_proofs isar_params num_chained one_line_params + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end, (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^ (if important_message <> "" then @@ -392,7 +389,8 @@ "")) end | SOME failure => - ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, "")) + ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed), + fn _ => string_of_atp_failure failure, "")) in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, message_tail = message_tail} diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 03 19:50:38 2014 +0100 @@ -8,8 +8,8 @@ signature SLEDGEHAMMER_PROVER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature - type reconstructor = Sledgehammer_Reconstructor.reconstructor - type play_outcome = Sledgehammer_Reconstructor.play_outcome + type proof_method = Sledgehammer_Proof_Methods.proof_method + type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type prover = Sledgehammer_Prover.prover @@ -23,11 +23,11 @@ val auto_minimize_min_facts : int Config.T val auto_minimize_max_time : real Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> - Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option -> + Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option - * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string) - * string) + * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string) + * string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list -> @@ -44,35 +44,31 @@ open ATP_Systems open Sledgehammer_Util open Sledgehammer_Fact -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT -fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) +fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) minimize_command ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) = let - val reconstr = - if name = metisN then - Metis (type_enc |> the_default (hd partial_type_encs), - lam_trans |> the_default default_metis_lam_trans) - else if name = smtN then - SMT - else - raise Fail ("unknown reconstructor: " ^ quote name) + val meth = + if name = metisN then Metis_Method (type_enc, lam_trans) + else if name = smtN then SMT_Method + else raise Fail ("unknown proof_method: " ^ quote name) val used_facts = facts |> map fst in (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts - state subgoal reconstr [reconstr] of + state subgoal meth [meth] of play as (_, Played time) => {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, preplay = Lazy.value play, message = fn play => let - val (_, override_params) = extract_reconstructor params reconstr + val (_, override_params) = extract_proof_method params meth val one_line_params = (play, proof_banner mode name, used_facts, minimize_command override_params name, subgoal, subgoal_count) @@ -93,18 +89,18 @@ fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in - is_reconstructor orf is_atp thy orf is_smt_prover ctxt + is_proof_method orf is_atp thy orf is_smt_prover ctxt end fun is_prover_installed ctxt = - is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) + is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) -val reconstructor_default_max_facts = 20 +val proof_method_default_max_facts = 20 fun default_max_facts_of_prover ctxt name = let val thy = Proof_Context.theory_of ctxt in - if is_reconstructor name then - reconstructor_default_max_facts + if is_proof_method name then + proof_method_default_max_facts else if is_atp thy name then fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0 else (* is_smt_prover ctxt name *) @@ -113,7 +109,7 @@ fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in - if is_reconstructor name then run_reconstructor mode name + if is_proof_method name then run_proof_method mode name else if is_atp thy name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name ^ ".") @@ -134,7 +130,7 @@ fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, - preplay_timeout, ...} : params) + smt_proofs, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state goal facts = let val _ = @@ -149,8 +145,8 @@ max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, - slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout, - expect = ""} + smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout, + preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} @@ -286,20 +282,21 @@ "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", "")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))) - handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, "")) + handle ERROR msg => + (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, "")) end -fun adjust_reconstructor_params override_params +fun adjust_proof_method_params override_params ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, - max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout, - preplay_timeout, expect} : params) = + max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize, + timeout, preplay_timeout, expect} : params) = let fun lookup_override name default_value = (case AList.lookup (op =) override_params name of SOME [s] => SOME s | _ => default_value) - (* Only those options that reconstructors are interested in are considered here. *) + (* Only those options that proof_methods are interested in are considered here. *) val type_enc = lookup_override "type_enc" type_enc val lam_trans = lookup_override "lam_trans" lam_trans in @@ -308,8 +305,8 @@ uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...}) @@ -336,18 +333,18 @@ fun prover_fast_enough () = can_min_fast_enough run_time in (case Lazy.force preplay of - (reconstr as Metis _, Played timeout) => + (meth as Metis_Method _, Played timeout) => if isar_proofs = SOME true then (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved itself. *) (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params)) else if can_min_fast_enough timeout then - (true, extract_reconstructor params reconstr + (true, extract_proof_method params meth ||> (fn override_params => - adjust_reconstructor_params override_params params)) + adjust_proof_method_params override_params params)) else (prover_fast_enough (), (name, params)) - | (SMT, Played timeout) => + | (SMT_Method, Played timeout) => (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved itself. *) (can_min_fast_enough timeout, (name, params)) diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:50:38 2014 +0100 @@ -38,7 +38,7 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Reconstructor +open Sledgehammer_Proof_Methods open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true) @@ -212,8 +212,8 @@ do_slice timeout 1 NONE Time.zeroTime end -fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command - ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = +fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...}) + minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -233,9 +233,8 @@ (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT - (bunch_of_reconstructors false (fn desperate => - if desperate then liftingN else default_metis_lam_trans))), + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let val one_line_params = @@ -248,7 +247,8 @@ end, if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") | SOME failure => - (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, "")) + (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), + fn _ => string_of_atp_failure failure, "")) in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, message_tail = message_tail} diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Feb 03 19:50:16 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML - Author: Jasmin Blanchette, TU Muenchen - Author: Steffen Juilf Smolka, TU Muenchen - -Reconstructors. -*) - -signature SLEDGEHAMMER_RECONSTRUCTOR = -sig - type stature = ATP_Problem_Generate.stature - - datatype reconstructor = - Metis of string * string | - SMT - - datatype play_outcome = - Played of Time.time | - Play_Timed_Out of Time.time | - Play_Failed | - Not_Played - - type minimize_command = string list -> string - type one_line_params = - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int - - val smtN : string - - val string_of_reconstructor : reconstructor -> string - val string_of_play_outcome : play_outcome -> string - val play_outcome_ord : play_outcome * play_outcome -> order - - val one_line_proof_text : int -> one_line_params -> string - val silence_reconstructors : bool -> Proof.context -> Proof.context -end; - -structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = -struct - -open ATP_Util -open ATP_Problem_Generate -open ATP_Proof_Reconstruct - -datatype reconstructor = - Metis of string * string | - SMT - -datatype play_outcome = - Played of Time.time | - Play_Timed_Out of Time.time | - Play_Failed | - Not_Played - -type minimize_command = string list -> string -type one_line_params = - (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int - -val smtN = "smt" - -fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | string_of_reconstructor SMT = smtN - -fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) - | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" - | string_of_play_outcome Play_Failed = "failed" - | string_of_play_outcome _ = "unknown" - -fun play_outcome_ord (Played time1, Played time2) = - int_ord (pairself Time.toMilliseconds (time1, time2)) - | play_outcome_ord (Played _, _) = LESS - | play_outcome_ord (_, Played _) = GREATER - | play_outcome_ord (Not_Played, Not_Played) = EQUAL - | play_outcome_ord (Not_Played, _) = LESS - | play_outcome_ord (_, Not_Played) = GREATER - | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = - int_ord (pairself Time.toMilliseconds (time1, time2)) - | play_outcome_ord (Play_Timed_Out _, _) = LESS - | play_outcome_ord (_, Play_Timed_Out _) = GREATER - | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL - -(* FIXME: Various bugs, esp. with "unfolding" -fun unusing_chained_facts _ 0 = "" - | unusing_chained_facts used_chaineds num_chained = - if length used_chaineds = num_chained then "" - else if null used_chaineds then "(* using no facts *) " - else "(* using only " ^ space_implode " " used_chaineds ^ " *) " -*) - -fun apply_on_subgoal _ 1 = "by " - | apply_on_subgoal 1 _ = "apply " - | apply_on_subgoal i n = - "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n - -fun command_call name [] = - name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" - | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" - -fun reconstructor_command reconstr i n used_chaineds num_chained ss = - (* unusing_chained_facts used_chaineds num_chained ^ *) - apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss - -fun show_time NONE = "" - | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" - -fun try_command_line banner time command = - banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "." - -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - (case minimize_command ss of - "" => "" - | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".") - -fun split_used_facts facts = - facts - |> List.partition (fn (_, (sc, _)) => sc = Chained) - |> pairself (sort_distinct (string_ord o pairself fst)) - -fun one_line_proof_text num_chained - ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = - let - val (chained, extra) = split_used_facts used_facts - - val (failed, ext_time) = - (case play of - Played time => (false, (SOME (false, time))) - | Play_Timed_Out time => (false, SOME (true, time)) - | Play_Failed => (true, NONE) - | Not_Played => (false, NONE)) - - val try_line = - map fst extra - |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained - |> (if failed then - enclose "One-line proof reconstruction failed: " - ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)" - else - try_command_line banner ext_time) - in - try_line ^ minimize_line minimize_command (map fst (extra @ chained)) - end - -(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification - bound exceeded" warnings and the like. *) -fun silence_reconstructors debug = - Try0.silence_methods debug - #> Config.put SMT_Config.verbose debug - -end; diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Feb 03 19:50:38 2014 +0100 @@ -69,10 +69,10 @@ | "" => SOME true | _ => raise Option.Option) handle Option.Option => - let val ss = map quote ((option ? cons "smart") ["true", "false"]) in - error ("Parameter " ^ quote name ^ " must be assigned " ^ - space_implode " " (serial_commas "or" ss) ^ ".") - end + let val ss = map quote ((option ? cons "smart") ["true", "false"]) in + error ("Parameter " ^ quote name ^ " must be assigned " ^ + space_implode " " (serial_commas "or" ss) ^ ".") + end val has_junk = exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *) @@ -80,8 +80,8 @@ fun parse_time name s = let val secs = if has_junk s then NONE else Real.fromString s in if is_none secs orelse Real.< (the secs, 0.0) then - error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \ - \number of seconds (e.g., \"60\", \"0.5\") or \"none\".") + error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \ + \(e.g., \"60\", \"0.5\") or \"none\".") else seconds (the secs) end diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Tools/Code/code_namespace.ML Mon Feb 03 19:50:38 2014 +0100 @@ -42,26 +42,42 @@ (** fundamental module name hierarchy **) -fun lookup_identifier identifiers sym = - Code_Symbol.lookup identifiers sym - |> Option.map (split_last o Long_Name.explode); +fun module_fragments' { identifiers, reserved } name = + case Code_Symbol.lookup_module_data identifiers name of + SOME (fragments, _) => fragments + | NONE => map (fn fragment => fst (Name.variant fragment reserved)) (Long_Name.explode name); + +fun module_fragments { module_name, identifiers, reserved } = + if module_name = "" + then module_fragments' { identifiers = identifiers, reserved = reserved } + else K (Long_Name.explode module_name); -fun force_identifier ctxt fragments_tab force_module identifiers sym = - case lookup_identifier identifiers sym of - NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym) +fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program = + let + val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; + val module_fragments' = module_fragments + { module_name = module_name, identifiers = identifiers, reserved = reserved }; + in + fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name)) + module_names Symtab.empty + end; + +fun prep_symbol ctxt { module_namespace, force_module, identifiers } sym = + case Code_Symbol.lookup identifiers sym of + NONE => ((the o Symtab.lookup module_namespace o Code_Symbol.default_prefix ctxt) sym, + Code_Symbol.default_base sym) | SOME prefix_name => if null force_module then prefix_name else (force_module, snd prefix_name); -fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program = - let - fun alias_fragments name = case module_identifiers name - of SOME name' => Long_Name.explode name' - | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name); - val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program []; - in - fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name)) - module_names Symtab.empty - end; +fun has_priority identifiers = is_some o Code_Symbol.lookup identifiers; + +fun build_proto_program { empty, add_stmt, add_dep } program = + empty + |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program + |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => + Code_Symbol.Graph.Keys.fold (add_dep sym) syms) program; + +fun prioritize has_priority = uncurry append o List.partition has_priority; (** flat program structure **) @@ -73,13 +89,12 @@ let (* building module name hierarchy *) - val module_identifiers = if module_name = "" - then Code_Symbol.lookup_module_data identifiers - else K (SOME module_name); - val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix, - module_identifiers = module_identifiers, reserved = reserved } program; - val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers + val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix, + module_name = module_name, identifiers = identifiers, reserved = reserved } program; + val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, + force_module = Long_Name.explode module_name, identifiers = identifiers } #>> Long_Name.implode; + val sym_priority = has_priority identifiers; (* distribute statements over hierarchy *) fun add_stmt sym stmt = @@ -89,7 +104,7 @@ Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt))) end; - fun add_dependency sym sym' = + fun add_dep sym sym' = let val (module_name, _) = prep_sym sym; val (module_name', _) = prep_sym sym'; @@ -97,10 +112,8 @@ then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym')) else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym')) end; - val proto_program = Graph.empty - |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program - |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => - Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program; + val proto_program = build_proto_program + { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program; (* name declarations and statement modifications *) fun declare sym (base, stmt) (gr, nsp) = @@ -109,7 +122,8 @@ val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; in (gr', nsp') end; fun declarations gr = (gr, empty_nsp) - |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr) + |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) + (prioritize sym_priority (Code_Symbol.Graph.keys gr)) |> fst |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt; val flat_program = proto_program @@ -165,12 +179,11 @@ let (* building module name hierarchy *) - val module_identifiers = if module_name = "" - then Code_Symbol.lookup_module_data identifiers - else K (SOME module_name); - val fragments_tab = build_module_namespace ctxt { module_prefix = "", - module_identifiers = module_identifiers, reserved = reserved } program; - val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers; + val module_namespace = build_module_namespace ctxt { module_prefix = "", + module_name = module_name, identifiers = identifiers, reserved = reserved } program; + val prep_sym = prep_symbol ctxt { module_namespace = module_namespace, + force_module = Long_Name.explode module_name, identifiers = identifiers } + val sym_priority = has_priority identifiers; (* building empty module hierarchy *) val empty_module = (empty_data, Code_Symbol.Graph.empty); @@ -184,9 +197,9 @@ #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments; val empty_program = empty_module - |> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab + |> Symtab.fold (fn (_, fragments) => allocate_module fragments) module_namespace |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst - o lookup_identifier identifiers o fst) program; + o Code_Symbol.lookup identifiers o fst) program; (* distribute statements over hierarchy *) fun add_stmt sym stmt = @@ -195,7 +208,7 @@ in (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt))) end; - fun add_dependency sym sym' = + fun add_dep sym sym' = let val (name_fragments, _) = prep_sym sym; val (name_fragments', _) = prep_sym sym'; @@ -211,17 +224,18 @@ ^ " would result in module dependency cycle")) else Code_Symbol.Graph.add_edge dep in (map_module name_fragments_common o apsnd) add_edge end; - val proto_program = empty_program - |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program - |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) => - Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program; + val proto_program = build_proto_program + { empty = empty_program, add_stmt = add_stmt, add_dep = add_dep } program; (* name declarations, data and statement modifications *) fun make_declarations nsps (data, nodes) = let - val (module_fragments, stmt_syms) = List.partition - (fn sym => case Code_Symbol.Graph.get_node nodes sym - of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes); + val (module_fragments, stmt_syms) = + Code_Symbol.Graph.keys nodes + |> List.partition + (fn sym => case Code_Symbol.Graph.get_node nodes sym + of (_, Module _) => true | _ => false) + |> pairself (prioritize sym_priority) fun declare namify sym (nsps, nodes) = let val (base, node) = Code_Symbol.Graph.get_node nodes sym; diff -r 70e7ac6af16f -r b1ca6ce9e1e0 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Feb 03 19:50:16 2014 +0100 +++ b/src/Tools/Code/code_target.ML Mon Feb 03 19:50:38 2014 +0100 @@ -81,7 +81,8 @@ class * (string * 'c option) list, (class * class) * (string * 'd option) list, (class * string) * (string * 'e option) list, string * (string * 'f option) list) Code_Symbol.attr; -type identifier_data = (string, string, string, string, string, string) Code_Symbol.data; +type identifier_data = (string list * string, string list * string, string list * string, string list * string, + string list * string, string list * string) Code_Symbol.data; type tyco_syntax = Code_Printer.tyco_syntax; type raw_const_syntax = Code_Printer.raw_const_syntax; @@ -144,7 +145,7 @@ val y' = Name.desymbolize false y; in ys' @ [y'] end; in if xs' = xs - then s + then if is_module then (xs, "") else split_last xs else error ("Invalid code name: " ^ quote s ^ "\n" ^ "better try " ^ quote (Long_Name.implode xs')) end; @@ -372,11 +373,12 @@ val width = the_default default_width some_width; in (fn program => prepared_serializer program width, prepared_program) end; -fun invoke_serializer thy target some_width module_name args program syms = +fun invoke_serializer thy target some_width raw_module_name args program syms = let - val check = if module_name = "" then I else check_name true; + val module_name = if raw_module_name = "" then "" + else (check_name true raw_module_name; raw_module_name) val (mounted_serializer, prepared_program) = mount_serializer thy - target some_width (check module_name) args program syms; + target some_width module_name args program syms; in mounted_serializer prepared_program end; fun assert_module_name "" = error "Empty module name not allowed here"