pass relevant options from "sledgehammer" to "sledgehammer minimize";
authorblanchet
Wed Apr 21 16:21:19 2010 +0200 (2010-04-21 ago)
changeset 36281dbbf4d5d584d
parent 36268 65aabc2c89ae
child 36282 9a7c5b86a105
pass relevant options from "sledgehammer" to "sledgehammer minimize";
one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 21 14:46:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 21 16:21:19 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  signature ATP_MANAGER =
     1.5  sig
     1.6    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     1.7 +  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
     1.8    type params =
     1.9      {debug: bool,
    1.10       verbose: bool,
    1.11 @@ -41,7 +42,8 @@
    1.12       proof: string,
    1.13       internal_thm_names: string Vector.vector,
    1.14       filtered_clauses: (thm * (string * int)) list}
    1.15 -  type prover = params -> Time.time -> problem -> prover_result
    1.16 +  type prover =
    1.17 +    params -> minimize_command -> Time.time -> problem -> prover_result
    1.18  
    1.19    val atps: string Unsynchronized.ref
    1.20    val timeout: int Unsynchronized.ref
    1.21 @@ -52,7 +54,9 @@
    1.22    val add_prover: string * prover -> theory -> theory
    1.23    val get_prover: theory -> string -> prover option
    1.24    val available_atps: theory -> unit
    1.25 -  val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
    1.26 +  val sledgehammer:
    1.27 +    params -> int -> relevance_override -> (string -> minimize_command)
    1.28 +    -> Proof.state -> unit
    1.29  end;
    1.30  
    1.31  structure ATP_Manager : ATP_MANAGER =
    1.32 @@ -62,7 +66,7 @@
    1.33  open Sledgehammer_Fact_Filter
    1.34  open Sledgehammer_Proof_Reconstruct
    1.35  
    1.36 -(** parameters, problems, results, and provers **)
    1.37 +(** problems, results, provers, etc. **)
    1.38  
    1.39  type params =
    1.40    {debug: bool,
    1.41 @@ -99,7 +103,8 @@
    1.42     internal_thm_names: string Vector.vector,
    1.43     filtered_clauses: (thm * (string * int)) list};
    1.44  
    1.45 -type prover = params -> Time.time -> problem -> prover_result;
    1.46 +type prover =
    1.47 +  params -> minimize_command -> Time.time -> problem -> prover_result
    1.48  
    1.49  
    1.50  (** preferences **)
    1.51 @@ -323,12 +328,12 @@
    1.52    val empty = Symtab.empty;
    1.53    val extend = I;
    1.54    fun merge data : T = Symtab.merge (eq_snd op =) data
    1.55 -    handle Symtab.DUP dup => err_dup_prover dup;
    1.56 +    handle Symtab.DUP name => err_dup_prover name;
    1.57  );
    1.58  
    1.59  fun add_prover (name, prover) thy =
    1.60    Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
    1.61 -    handle Symtab.DUP dup => err_dup_prover dup;
    1.62 +    handle Symtab.DUP name => err_dup_prover name;
    1.63  
    1.64  fun get_prover thy name =
    1.65    Option.map #1 (Symtab.lookup (Provers.get thy) name);
    1.66 @@ -341,7 +346,7 @@
    1.67  (* start prover thread *)
    1.68  
    1.69  fun start_prover (params as {timeout, ...}) birth_time death_time i
    1.70 -                 relevance_override proof_state name =
    1.71 +                 relevance_override minimize_command proof_state name =
    1.72    (case get_prover (Proof.theory_of proof_state) name of
    1.73      NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
    1.74    | SOME prover =>
    1.75 @@ -359,7 +364,8 @@
    1.76                {subgoal = i, goal = (ctxt, (facts, goal)),
    1.77                 relevance_override = relevance_override, axiom_clauses = NONE,
    1.78                 filtered_clauses = NONE}
    1.79 -            val message = #message (prover params timeout problem)
    1.80 +            val message =
    1.81 +              #message (prover params (minimize_command name) timeout problem)
    1.82                handle Sledgehammer_HOL_Clause.TRIVIAL =>
    1.83                    metis_line i n []
    1.84                  | ERROR msg => "Error: " ^ msg ^ ".\n";
    1.85 @@ -371,14 +377,15 @@
    1.86  (* Sledgehammer the given subgoal *)
    1.87  
    1.88  fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
    1.89 -                 proof_state =
    1.90 +                 minimize_command proof_state =
    1.91    let
    1.92      val birth_time = Time.now ()
    1.93      val death_time = Time.+ (birth_time, timeout)
    1.94      val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
    1.95      val _ = priority "Sledgehammering..."
    1.96      val _ = List.app (start_prover params birth_time death_time i
    1.97 -                                   relevance_override proof_state) atps
    1.98 +                                   relevance_override minimize_command
    1.99 +                                   proof_state) atps
   1.100    in () end
   1.101  
   1.102  end;
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 14:46:29 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 21 16:21:19 2010 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4        axiom_clauses = SOME axclauses,
     2.5        filtered_clauses = SOME (the_default axclauses filtered_clauses)}
     2.6    in
     2.7 -    `outcome_of_result (prover params timeout problem)
     2.8 +    `outcome_of_result (prover params (K "") timeout problem)
     2.9      |>> tap (priority o string_of_outcome)
    2.10    end
    2.11  
    2.12 @@ -122,8 +122,8 @@
    2.13              ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
    2.14          in
    2.15            (SOME min_thms,
    2.16 -           proof_text isar_proof true modulus sorts atp_name proof
    2.17 -                      internal_thm_names ctxt goal i |> fst)
    2.18 +           proof_text isar_proof modulus sorts ctxt (K "") proof
    2.19 +                      internal_thm_names goal i |> fst)
    2.20          end
    2.21      | (Timeout, _) =>
    2.22          (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 14:46:29 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 16:21:19 2010 +0200
     3.3 @@ -73,6 +73,7 @@
     3.4  
     3.5  fun generic_prover overlord get_facts prepare write_file cmd args known_failures
     3.6          proof_text name ({debug, full_types, explicit_apply, ...} : params)
     3.7 +        minimize_command
     3.8          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
     3.9           : problem) =
    3.10    let
    3.11 @@ -105,7 +106,7 @@
    3.12        in
    3.13          if destdir' = "" then File.tmp_path probfile
    3.14          else if File.exists (Path.explode destdir')
    3.15 -        then Path.append  (Path.explode destdir') probfile
    3.16 +        then Path.append (Path.explode destdir') probfile
    3.17          else error ("No such directory: " ^ destdir' ^ ".")
    3.18        end;
    3.19  
    3.20 @@ -154,7 +155,7 @@
    3.21      val success = rc = 0 andalso failure = "";
    3.22      val (message, relevant_thm_names) =
    3.23        if success then
    3.24 -        proof_text name proof internal_thm_names ctxt th subgoal
    3.25 +        proof_text ctxt minimize_command proof internal_thm_names th subgoal
    3.26        else if failure <> "" then
    3.27          (failure, [])
    3.28        else
    3.29 @@ -176,7 +177,7 @@
    3.30          (params as {debug, overlord, respect_no_atp, relevance_threshold,
    3.31                      convergence, theory_relevant, higher_order, follow_defs,
    3.32                      isar_proof, modulus, sorts, ...})
    3.33 -        timeout =
    3.34 +        minimize_command timeout =
    3.35    generic_prover overlord
    3.36        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.37                            higher_order follow_defs max_new_clauses
    3.38 @@ -184,8 +185,8 @@
    3.39        (prepare_clauses higher_order false)
    3.40        (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
    3.41        (arguments timeout) known_failures
    3.42 -      (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
    3.43 -      name params
    3.44 +      (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts)
    3.45 +      name params minimize_command
    3.46  
    3.47  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    3.48  
    3.49 @@ -240,14 +241,14 @@
    3.50                   prefers_theory_relevant, ...} : prover_config))
    3.51          (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    3.52                      theory_relevant, higher_order, follow_defs, ...})
    3.53 -        timeout =
    3.54 +        minimize_command timeout =
    3.55    generic_prover overlord
    3.56        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.57                            higher_order follow_defs max_new_clauses
    3.58                            (the_default prefers_theory_relevant theory_relevant))
    3.59        (prepare_clauses higher_order true) write_dfg_file command
    3.60 -      (arguments timeout) known_failures (metis_proof_text false false)
    3.61 -      name params
    3.62 +      (arguments timeout) known_failures (K metis_proof_text)
    3.63 +      name params minimize_command
    3.64  
    3.65  fun dfg_prover name p = (name, generic_dfg_prover (name, p))
    3.66  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 14:46:29 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 21 16:21:19 2010 +0200
     4.3 @@ -68,6 +68,10 @@
     4.4     ("metis_proof", "isar_proof"),
     4.5     ("no_sorts", "sorts")]
     4.6  
     4.7 +val params_for_minimize =
     4.8 +  ["full_types", "explicit_apply", "higher_order", "isar_proof", "modulus",
     4.9 +   "sorts", "minimize_timeout"]
    4.10 +
    4.11  val property_dependent_params = ["atps", "full_types", "timeout"]
    4.12  
    4.13  fun is_known_raw_param s =
    4.14 @@ -219,18 +223,33 @@
    4.15  val refresh_tptpN = "refresh_tptp"
    4.16  val helpN = "help"
    4.17  
    4.18 -
    4.19  fun minimizize_raw_param_name "timeout" = "minimize_timeout"
    4.20    | minimizize_raw_param_name name = name
    4.21  
    4.22 +val is_raw_param_relevant_for_minimize =
    4.23 +  member (op =) params_for_minimize o fst o unalias_raw_param
    4.24 +fun string_for_raw_param (key, values) =
    4.25 +  key ^ (case space_implode " " values of
    4.26 +           "" => ""
    4.27 +         | value => " = " ^ value)
    4.28 +
    4.29 +fun minimize_command override_params i atp_name facts =
    4.30 +  "sledgehammer minimize [atp = " ^ atp_name ^
    4.31 +  (override_params |> filter is_raw_param_relevant_for_minimize
    4.32 +                   |> implode o map (prefix ", " o string_for_raw_param)) ^
    4.33 +  "] (" ^ space_implode " " facts ^ ")" ^
    4.34 +  (if i = 1 then "" else " " ^ string_of_int i)
    4.35 +
    4.36  fun hammer_away override_params subcommand opt_i relevance_override state =
    4.37    let
    4.38      val thy = Proof.theory_of state
    4.39      val _ = List.app check_raw_param override_params
    4.40    in
    4.41      if subcommand = runN then
    4.42 -      sledgehammer (get_params thy override_params) (the_default 1 opt_i)
    4.43 -                   relevance_override state
    4.44 +      let val i = the_default 1 opt_i in
    4.45 +        sledgehammer (get_params thy override_params) i relevance_override
    4.46 +                     (minimize_command override_params i) state
    4.47 +      end
    4.48      else if subcommand = minimizeN then
    4.49        minimize (map (apfst minimizize_raw_param_name) override_params) []
    4.50                 (the_default 1 opt_i) (#add relevance_override) state
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 14:46:29 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 21 16:21:19 2010 +0200
     5.3 @@ -6,6 +6,8 @@
     5.4  
     5.5  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     5.6  sig
     5.7 +  type minimize_command = string list -> string
     5.8 +
     5.9    val chained_hint: string
    5.10    val invert_const: string -> string
    5.11    val invert_type_const: string -> string
    5.12 @@ -15,14 +17,14 @@
    5.13    val is_proof_well_formed: string -> bool
    5.14    val metis_line: int -> int -> string list -> string
    5.15    val metis_proof_text:
    5.16 -    bool -> bool -> string -> string -> string vector -> Proof.context -> thm
    5.17 -    -> int -> string * string list
    5.18 +    minimize_command -> string -> string vector -> thm -> int
    5.19 +    -> string * string list
    5.20    val isar_proof_text:
    5.21 -    bool -> int -> bool -> string -> string -> string vector -> Proof.context
    5.22 +    int -> bool -> Proof.context -> minimize_command -> string -> string vector
    5.23      -> thm -> int -> string * string list
    5.24    val proof_text:
    5.25 -    bool -> bool -> int -> bool -> string -> string -> string vector
    5.26 -    -> Proof.context -> thm -> int -> string * string list
    5.27 +    bool -> int -> bool -> Proof.context -> minimize_command -> string
    5.28 +    -> string vector -> thm -> int -> string * string list
    5.29  end;
    5.30  
    5.31  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    5.32 @@ -31,6 +33,8 @@
    5.33  open Sledgehammer_FOL_Clause
    5.34  open Sledgehammer_Fact_Preprocessor
    5.35  
    5.36 +type minimize_command = string list -> string
    5.37 +
    5.38  val trace_proof_path = Path.basic "atp_trace";
    5.39  
    5.40  fun trace_proof_msg f =
    5.41 @@ -528,16 +532,15 @@
    5.42  fun metis_line i n xs =
    5.43    "Try this command: " ^
    5.44    Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
    5.45 -fun minimize_line _ _ [] = ""
    5.46 -  | minimize_line isar_proof atp_name xs =
    5.47 +fun minimize_line _ [] = ""
    5.48 +  | minimize_line minimize_command facts =
    5.49 +    case minimize_command facts of
    5.50 +      "" => ""
    5.51 +    | command =>
    5.52        "To minimize the number of lemmas, try this command: " ^
    5.53 -      Markup.markup Markup.sendback
    5.54 -                    ("sledgehammer minimize [atp = " ^ atp_name ^
    5.55 -                     (if isar_proof then ", isar_proof" else "") ^ "] (" ^
    5.56 -                     space_implode " " xs ^ ")") ^ ".\n"
    5.57 +      Markup.markup Markup.sendback command ^ ".\n"
    5.58  
    5.59 -fun metis_proof_text isar_proof minimal atp_name proof thm_names
    5.60 -                     (_ : Proof.context) goal i =
    5.61 +fun metis_proof_text minimize_command proof thm_names goal i =
    5.62    let
    5.63      val lemmas =
    5.64        proof |> get_proof_extract
    5.65 @@ -549,12 +552,10 @@
    5.66      val n = Logic.count_prems (prop_of goal)
    5.67      val xs = kill_chained lemmas
    5.68    in
    5.69 -    (metis_line i n xs ^
    5.70 -     (if minimal then "" else minimize_line isar_proof atp_name xs),
    5.71 -     kill_chained lemmas)
    5.72 +    (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
    5.73    end
    5.74  
    5.75 -fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i =
    5.76 +fun isar_proof_text modulus sorts ctxt minimize_command proof thm_names goal i =
    5.77    let
    5.78      (* We could use "split_lines", but it can return blank lines. *)
    5.79      val lines = String.tokens (equal #"\n");
    5.80 @@ -563,7 +564,7 @@
    5.81      val extract = get_proof_extract proof
    5.82      val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
    5.83      val (one_line_proof, lemma_names) =
    5.84 -      metis_proof_text true minimal atp_name proof thm_names ctxt goal i
    5.85 +      metis_proof_text minimize_command proof thm_names goal i
    5.86      val tokens = String.tokens (fn c => c = #" ") one_line_proof
    5.87      val isar_proof =
    5.88        if member (op =) tokens chained_hint then ""
    5.89 @@ -575,8 +576,7 @@
    5.90       lemma_names)
    5.91    end
    5.92  
    5.93 -fun proof_text isar_proof minimal modulus sorts =
    5.94 -  if isar_proof then isar_proof_text minimal modulus sorts
    5.95 -  else metis_proof_text isar_proof minimal
    5.96 +fun proof_text isar_proof modulus sorts ctxt =
    5.97 +  if isar_proof then isar_proof_text modulus sorts ctxt else metis_proof_text
    5.98  
    5.99  end;