make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
authorblanchet
Mon Mar 29 18:44:24 2010 +0200 (2010-03-29 ago)
changeset 36063cdc6855a6387
parent 36062 194cb6e3c13f
child 36064 48aec67c284f
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.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	Mon Mar 29 15:50:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 18:44:24 2010 +0200
     1.3 @@ -54,7 +54,8 @@
     1.4  structure ATP_Manager : ATP_MANAGER =
     1.5  struct
     1.6  
     1.7 -type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     1.8 +open Sledgehammer_Fact_Filter
     1.9 +open Sledgehammer_Proof_Reconstruct
    1.10  
    1.11  (** parameters, problems, results, and provers **)
    1.12  
    1.13 @@ -322,6 +323,7 @@
    1.14    | SOME prover =>
    1.15        let
    1.16          val {context = ctxt, facts, goal} = Proof.goal proof_state;
    1.17 +        val n = Logic.count_prems (prop_of goal)
    1.18          val desc =
    1.19            "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
    1.20              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
    1.21 @@ -334,9 +336,8 @@
    1.22                 relevance_override = relevance_override, axiom_clauses = NONE,
    1.23                 filtered_clauses = NONE}
    1.24              val message = #message (prover params timeout problem)
    1.25 -              handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
    1.26 -                  "Try this command: " ^
    1.27 -                  Markup.markup Markup.sendback "by metis" ^ "."
    1.28 +              handle Sledgehammer_HOL_Clause.TRIVIAL =>
    1.29 +                  metis_line i n []
    1.30                  | ERROR msg => ("Error: " ^ msg);
    1.31              val _ = unregister message (Thread.self ());
    1.32            in () end);
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 29 15:50:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 29 18:44:24 2010 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4    val linear_minimize : 'a minimize_fun
     2.5    val binary_minimize : 'a minimize_fun
     2.6    val minimize_theorems :
     2.7 -    params -> (string * thm list) minimize_fun -> prover -> string
     2.8 +    params -> (string * thm list) minimize_fun -> prover -> string -> int
     2.9      -> Proof.state -> (string * thm list) list
    2.10      -> (string * thm list) list option * string
    2.11  end;
    2.12 @@ -23,6 +23,7 @@
    2.13  struct
    2.14  
    2.15  open Sledgehammer_Fact_Preprocessor
    2.16 +open Sledgehammer_Proof_Reconstruct
    2.17  open ATP_Manager
    2.18  
    2.19  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    2.20 @@ -111,7 +112,7 @@
    2.21  (* wrapper for calling external prover *)
    2.22  
    2.23  fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
    2.24 -        timeout subgoalno state filtered name_thms_pairs =
    2.25 +        timeout subgoal state filtered name_thms_pairs =
    2.26    let
    2.27      val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
    2.28                        " theorems... ")
    2.29 @@ -119,7 +120,7 @@
    2.30      val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
    2.31      val {context = ctxt, facts, goal} = Proof.goal state
    2.32      val problem =
    2.33 -     {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
    2.34 +     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    2.35        relevance_override = {add = [], del = [], only = false},
    2.36        axiom_clauses = SOME axclauses, filtered_clauses = filtered}
    2.37      val (result, proof) = produce_answer (prover params timeout problem)
    2.38 @@ -130,7 +131,7 @@
    2.39  (* minimalization of thms *)
    2.40  
    2.41  fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
    2.42 -                      prover_name state name_thms_pairs =
    2.43 +                      prover_name i state name_thms_pairs =
    2.44    let
    2.45      val msecs = Time.toMilliseconds minimize_timeout
    2.46      val _ =
    2.47 @@ -138,9 +139,10 @@
    2.48          " theorems, ATP: " ^ prover_name ^
    2.49          ", time limit: " ^ string_of_int msecs ^ " ms")
    2.50      val test_thms_fun =
    2.51 -      sledgehammer_test_theorems params prover minimize_timeout 1 state
    2.52 +      sledgehammer_test_theorems params prover minimize_timeout i state
    2.53      fun test_thms filtered thms =
    2.54        case test_thms_fun filtered thms of (Success _, _) => true | _ => false
    2.55 +    val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems
    2.56    in
    2.57      (* try prove first to check result and get used theorems *)
    2.58      (case test_thms_fun NONE name_thms_pairs of
    2.59 @@ -157,13 +159,7 @@
    2.60            val min_names = sort_distinct string_ord (map fst min_thms)
    2.61            val _ = priority (cat_lines
    2.62              ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
    2.63 -        in
    2.64 -          (SOME min_thms,
    2.65 -           "Try this command: " ^
    2.66 -           Markup.markup Markup.sendback
    2.67 -                         ("by (metis " ^ space_implode " " min_names ^ ")")
    2.68 -           ^ ".")
    2.69 -        end
    2.70 +        in (SOME min_thms, metis_line i n min_names) end
    2.71      | (Timeout, _) =>
    2.72          (NONE, "Timeout: You may need to increase the time limit of " ^
    2.73            string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
    2.74 @@ -172,8 +168,7 @@
    2.75      | (Failure, _) =>
    2.76          (NONE, "Failure: No proof with the theorems supplied"))
    2.77      handle Sledgehammer_HOL_Clause.TRIVIAL =>
    2.78 -        (SOME [], "Trivial: Try this command: " ^
    2.79 -                  Markup.markup Markup.sendback "by metis" ^ ".")
    2.80 +        (SOME [], metis_line i n [])
    2.81        | ERROR msg => (NONE, "Error: " ^ msg)
    2.82    end
    2.83  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:50:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 18:44:24 2010 +0200
     3.3 @@ -80,6 +80,8 @@
     3.4  structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
     3.5  struct
     3.6  
     3.7 +open Sledgehammer_Util
     3.8 +
     3.9  val schematic_var_prefix = "V_";
    3.10  val fixed_var_prefix = "v_";
    3.11  
    3.12 @@ -184,8 +186,7 @@
    3.13     solved in 3.7 and perhaps in earlier versions too.) *)
    3.14  (* 32-bit hash, so we expect no collisions. *)
    3.15  fun controlled_length dfg s =
    3.16 -  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0))
    3.17 -  else s;
    3.18 +  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s;
    3.19  
    3.20  fun lookup_const dfg c =
    3.21      case Symtab.lookup const_trans_table c of
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 15:50:18 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 18:44:24 2010 +0200
     4.3 @@ -144,7 +144,7 @@
     4.4  fun get_params thy = extract_params thy (default_raw_params thy)
     4.5  fun default_params thy = get_params thy o map (apsnd single)
     4.6  
     4.7 -fun atp_minimize_command override_params old_style_args fact_refs state =
     4.8 +fun atp_minimize_command override_params old_style_args i fact_refs state =
     4.9    let
    4.10      val thy = Proof.theory_of state
    4.11      val ctxt = Proof.context_of state
    4.12 @@ -176,7 +176,7 @@
    4.13        | NONE => error ("Unknown ATP: " ^ quote atp))
    4.14      val name_thms_pairs = theorems_from_refs ctxt fact_refs
    4.15    in
    4.16 -    writeln (#2 (minimize_theorems params linear_minimize prover atp state
    4.17 +    writeln (#2 (minimize_theorems params linear_minimize prover atp i state
    4.18                                     name_thms_pairs))
    4.19    end
    4.20  
    4.21 @@ -202,7 +202,8 @@
    4.22        sledgehammer (get_params thy override_params) (the_default 1 opt_i)
    4.23                     relevance_override state
    4.24      else if subcommand = minimizeN then
    4.25 -      atp_minimize_command override_params [] (#add relevance_override) state
    4.26 +      atp_minimize_command override_params [] (the_default 1 opt_i)
    4.27 +                           (#add relevance_override) state
    4.28      else if subcommand = messagesN then
    4.29        messages opt_i
    4.30      else if subcommand = available_atpsN then
    4.31 @@ -287,7 +288,7 @@
    4.32      "minimize theorem list with external prover" K.diag
    4.33      (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
    4.34        Toplevel.no_timing o Toplevel.unknown_proof o
    4.35 -        Toplevel.keep (atp_minimize_command [] args fact_refs
    4.36 +        Toplevel.keep (atp_minimize_command [] args 1 fact_refs
    4.37                         o Toplevel.proof_of)))
    4.38  
    4.39  val _ =
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 15:50:18 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 18:44:24 2010 +0200
     5.3 @@ -14,6 +14,7 @@
     5.4    val strip_prefix: string -> string -> string option
     5.5    val setup: theory -> theory
     5.6    val is_proof_well_formed: string -> bool
     5.7 +  val metis_line: int -> int -> string list -> string
     5.8    val metis_lemma_list: bool -> string ->
     5.9      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
    5.10    val structured_isar_proof: string ->
    5.11 @@ -427,12 +428,15 @@
    5.12                 stringify_deps thm_names ((lno,lname)::deps_map) lines
    5.13             end;
    5.14  
    5.15 -val proofstart = "proof (neg_clausify)\n";
    5.16 +fun isar_proof_start i =
    5.17 +  (if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^
    5.18 +  "proof (neg_clausify)\n";
    5.19 +fun isar_fixes [] = ""
    5.20 +  | isar_fixes ts = "  fix " ^ space_implode " " ts ^ "\n";
    5.21 +fun isar_proof_end 1 = "qed"
    5.22 +  | isar_proof_end _ = "next"
    5.23  
    5.24 -fun isar_header [] = proofstart
    5.25 -  | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
    5.26 -
    5.27 -fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
    5.28 +fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names =
    5.29    let
    5.30      val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
    5.31      val tuples = map (dest_tstp o tstp_line o explode) cnfs
    5.32 @@ -448,7 +452,7 @@
    5.33      val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
    5.34      val _ = trace_proof_msg (fn () =>
    5.35        Int.toString (length lines) ^ " lines extracted\n")
    5.36 -    val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
    5.37 +    val (ccls, fixes) = neg_conjecture_clauses ctxt goal i
    5.38      val _ = trace_proof_msg (fn () =>
    5.39        Int.toString (length ccls) ^ " conjecture clauses\n")
    5.40      val ccls = map forall_intr_vars ccls
    5.41 @@ -456,8 +460,12 @@
    5.42                                (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
    5.43      val body = isar_proof_body ctxt (map prop_of ccls)
    5.44                                 (stringify_deps thm_names [] lines)
    5.45 +    val n = Logic.count_prems (prop_of goal)
    5.46      val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
    5.47 -  in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
    5.48 +  in
    5.49 +    isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^
    5.50 +    isar_proof_end n ^ "\n"
    5.51 +  end
    5.52    handle STREE _ => error "Could not extract proof (ATP output malformed?)";
    5.53  
    5.54  
    5.55 @@ -534,22 +542,30 @@
    5.56  val chained_hint = "CHAINED";
    5.57  val kill_chained = filter_out (curry (op =) chained_hint)
    5.58  
    5.59 -(* metis-command *)
    5.60 -fun metis_line [] = "by metis"
    5.61 -  | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
    5.62 -
    5.63 +fun apply_command _ 1 = "by "
    5.64 +  | apply_command 1 _ = "apply "
    5.65 +  | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
    5.66 +fun metis_command i n [] =
    5.67 +    apply_command i n ^ "metis"
    5.68 +  | metis_command i n xs =
    5.69 +    apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
    5.70 +fun metis_line i n xs =
    5.71 +  "Try this command: " ^
    5.72 +  Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
    5.73  fun minimize_line _ [] = ""
    5.74 -  | minimize_line name lemmas =
    5.75 +  | minimize_line name xs =
    5.76        "To minimize the number of lemmas, try this command:\n" ^
    5.77        Markup.markup Markup.sendback
    5.78                      ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
    5.79 -                     space_implode " " (kill_chained lemmas) ^ ")") ^ "."
    5.80 +                     space_implode " " xs ^ ")") ^ "."
    5.81  
    5.82 -fun metis_lemma_list dfg name result =
    5.83 -  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
    5.84 -    ("Try this command: " ^
    5.85 -     Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
    5.86 -     minimize_line name lemmas ^
    5.87 +fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) =
    5.88 +  let
    5.89 +    val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
    5.90 +    val n = Logic.count_prems (prop_of goal)
    5.91 +    val xs = kill_chained lemmas
    5.92 +  in
    5.93 +    (metis_line subgoalno n xs ^ minimize_line name xs ^
    5.94       (if used_conj then
    5.95          ""
    5.96        else
    5.97 @@ -572,11 +588,8 @@
    5.98        if member (op =) tokens chained_hint then ""
    5.99        else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
   5.100    in
   5.101 -    (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
   5.102 -       for a strange ProofGeneral bug, whereby the first two letters of the word
   5.103 -       "proof" are not highlighted. *)
   5.104 -    (one_line_proof ^ "\n\nStructured proof:" ^
   5.105 -     Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
   5.106 +    (one_line_proof ^ "\nStructured proof:\n" ^
   5.107 +     Markup.markup Markup.sendback isar_proof, lemma_names)
   5.108    end
   5.109  
   5.110  end;