added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
authorblanchet
Mon Mar 29 19:49:57 2010 +0200 (2010-03-29)
changeset 3606448aec67c284f
parent 36063 cdc6855a6387
child 36065 3fc077c4780a
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP_Manager/atp_manager.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/Sledgehammer.thy	Mon Mar 29 18:44:24 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Mar 29 19:49:57 2010 +0200
     1.3 @@ -99,7 +99,6 @@
     1.4  setup Sledgehammer_Fact_Preprocessor.setup
     1.5  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
     1.6  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
     1.7 -setup Sledgehammer_Proof_Reconstruct.setup
     1.8  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
     1.9  use "Tools/ATP_Manager/atp_manager.ML"
    1.10  use "Tools/ATP_Manager/atp_wrapper.ML"
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 18:44:24 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 19:49:57 2010 +0200
     2.3 @@ -21,6 +21,8 @@
     2.4       higher_order: bool option,
     2.5       follow_defs: bool,
     2.6       isar_proof: bool,
     2.7 +     modulus: int,
     2.8 +     sorts: bool,
     2.9       timeout: Time.time,
    2.10       minimize_timeout: Time.time}
    2.11    type problem =
    2.12 @@ -71,6 +73,8 @@
    2.13     higher_order: bool option,
    2.14     follow_defs: bool,
    2.15     isar_proof: bool,
    2.16 +   modulus: int,
    2.17 +   sorts: bool,
    2.18     timeout: Time.time,
    2.19     minimize_timeout: Time.time}
    2.20  
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 29 18:44:24 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 29 19:49:57 2010 +0200
     3.3 @@ -160,7 +160,8 @@
     3.4          (name, {command, arguments, failure_strs, max_new_clauses,
     3.5                  prefers_theory_const, supports_isar_proofs})
     3.6          (params as {respect_no_atp, relevance_threshold, convergence,
     3.7 -                    theory_const, higher_order, follow_defs, isar_proof, ...})
     3.8 +                    theory_const, higher_order, follow_defs, isar_proof,
     3.9 +                    modulus, sorts, ...})
    3.10          timeout =
    3.11    generic_prover
    3.12        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.13 @@ -168,8 +169,10 @@
    3.14                            (the_default prefers_theory_const theory_const))
    3.15        (prepare_clauses higher_order false) write_tptp_file command
    3.16        (arguments timeout) failure_strs
    3.17 -      (if supports_isar_proofs andalso isar_proof then structured_isar_proof
    3.18 -       else metis_lemma_list false) name params;
    3.19 +      (if supports_isar_proofs andalso isar_proof then
    3.20 +         structured_isar_proof modulus sorts
    3.21 +       else
    3.22 +         metis_lemma_list false) name params;
    3.23  
    3.24  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    3.25  
    3.26 @@ -215,7 +218,7 @@
    3.27          (name, ({command, arguments, failure_strs, max_new_clauses,
    3.28                   prefers_theory_const, ...} : prover_config))
    3.29          (params as {respect_no_atp, relevance_threshold, convergence,
    3.30 -                    theory_const, higher_order, follow_defs, isar_proof, ...})
    3.31 +                    theory_const, higher_order, follow_defs, ...})
    3.32          timeout =
    3.33    generic_prover
    3.34        (get_relevant_facts respect_no_atp relevance_threshold convergence
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 18:44:24 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 19:49:57 2010 +0200
     4.3 @@ -47,6 +47,8 @@
     4.4     ("higher_order", "smart"),
     4.5     ("follow_defs", "false"),
     4.6     ("isar_proof", "false"),
     4.7 +   ("modulus", "1"),
     4.8 +   ("sorts", "false"),
     4.9     ("minimize_timeout", "5 s")]
    4.10  
    4.11  val negated_params =
    4.12 @@ -57,7 +59,8 @@
    4.13     ("no_theory_const", "theory_const"),
    4.14     ("first_order", "higher_order"),
    4.15     ("dont_follow_defs", "follow_defs"),
    4.16 -   ("metis_proof", "isar_proof")]
    4.17 +   ("metis_proof", "isar_proof"),
    4.18 +   ("no_sorts", "sorts")]
    4.19  
    4.20  val property_dependent_params = ["atps", "full_types", "timeout"]
    4.21  
    4.22 @@ -130,6 +133,8 @@
    4.23      val higher_order = lookup_bool_option "higher_order"
    4.24      val follow_defs = lookup_bool "follow_defs"
    4.25      val isar_proof = lookup_bool "isar_proof"
    4.26 +    val modulus = Int.max (1, lookup_int "modulus")
    4.27 +    val sorts = lookup_bool "sorts"
    4.28      val timeout = lookup_time "timeout"
    4.29      val minimize_timeout = lookup_time "minimize_timeout"
    4.30    in
    4.31 @@ -137,8 +142,8 @@
    4.32       respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    4.33       convergence = convergence, theory_const = theory_const,
    4.34       higher_order = higher_order, follow_defs = follow_defs,
    4.35 -     isar_proof = isar_proof, timeout = timeout,
    4.36 -     minimize_timeout = minimize_timeout}
    4.37 +     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
    4.38 +     timeout = timeout, minimize_timeout = minimize_timeout}
    4.39    end
    4.40  
    4.41  fun get_params thy = extract_params thy (default_raw_params thy)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 18:44:24 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 19:49:57 2010 +0200
     5.3 @@ -12,12 +12,11 @@
     5.4    val num_typargs: theory -> string -> int
     5.5    val make_tvar: string -> typ
     5.6    val strip_prefix: string -> string -> string option
     5.7 -  val setup: theory -> theory
     5.8    val is_proof_well_formed: string -> bool
     5.9    val metis_line: int -> int -> string list -> string
    5.10    val metis_lemma_list: bool -> string ->
    5.11      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
    5.12 -  val structured_isar_proof: string ->
    5.13 +  val structured_isar_proof: int -> bool -> string ->
    5.14      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
    5.15  end;
    5.16  
    5.17 @@ -34,14 +33,6 @@
    5.18  
    5.19  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
    5.20  
    5.21 -(*For generating structured proofs: keep every nth proof line*)
    5.22 -val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1);
    5.23 -
    5.24 -(*Indicates whether to include sort information in generated proofs*)
    5.25 -val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true);
    5.26 -
    5.27 -val setup = modulus_setup #> recon_sorts_setup;
    5.28 -
    5.29  (**** PARSING OF TSTP FORMAT ****)
    5.30  
    5.31  (*Syntax trees, either termlist or formulae*)
    5.32 @@ -336,10 +327,13 @@
    5.33  
    5.34  (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
    5.35    ATP may have their literals reordered.*)
    5.36 -fun isar_proof_body ctxt ctms =
    5.37 +fun isar_proof_body ctxt sorts ctms =
    5.38    let
    5.39      val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
    5.40 -    val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
    5.41 +    val string_of_term = 
    5.42 +      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    5.43 +                              (print_mode_value ()))
    5.44 +                      (Syntax.string_of_term ctxt)
    5.45      fun have_or_show "show" _ = "  show \""
    5.46        | have_or_show have lname = "  " ^ have ^ " " ^ lname ^ ": \""
    5.47      fun do_line _ (lname, t, []) =
    5.48 @@ -355,7 +349,7 @@
    5.49      fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
    5.50        | do_lines ((lname, t, deps) :: lines) =
    5.51          do_line "have" (lname, t, deps) :: do_lines lines
    5.52 -  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
    5.53 +  in setmp_CRITICAL show_sorts sorts do_lines end;
    5.54  
    5.55  fun unequal t (_, t', _) = not (t aconv t');
    5.56  
    5.57 @@ -405,13 +399,13 @@
    5.58    counts the number of proof lines processed so far.
    5.59    Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
    5.60    phase may delete some dependencies, hence this phase comes later.*)
    5.61 -fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
    5.62 +fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) =
    5.63        (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
    5.64 -  | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
    5.65 +  | add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) =
    5.66        if eq_types t orelse not (null (Term.add_tvars t [])) orelse
    5.67           exists_subterm bad_free t orelse
    5.68           (not (null lines) andalso   (*final line can't be deleted for these reasons*)
    5.69 -          (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))
    5.70 +          (length deps < 2 orelse nlines mod modulus <> 0))
    5.71        then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
    5.72        else (nlines+1, (lno, t, deps) :: lines);
    5.73  
    5.74 @@ -436,7 +430,7 @@
    5.75  fun isar_proof_end 1 = "qed"
    5.76    | isar_proof_end _ = "next"
    5.77  
    5.78 -fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names =
    5.79 +fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names =
    5.80    let
    5.81      val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
    5.82      val tuples = map (dest_tstp o tstp_line o explode) cnfs
    5.83 @@ -449,7 +443,7 @@
    5.84      val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
    5.85      val _ = trace_proof_msg (fn () =>
    5.86        Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
    5.87 -    val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
    5.88 +    val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines
    5.89      val _ = trace_proof_msg (fn () =>
    5.90        Int.toString (length lines) ^ " lines extracted\n")
    5.91      val (ccls, fixes) = neg_conjecture_clauses ctxt goal i
    5.92 @@ -458,7 +452,7 @@
    5.93      val ccls = map forall_intr_vars ccls
    5.94      val _ = app (fn th => trace_proof_msg
    5.95                                (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
    5.96 -    val body = isar_proof_body ctxt (map prop_of ccls)
    5.97 +    val body = isar_proof_body ctxt sorts (map prop_of ccls)
    5.98                                 (stringify_deps thm_names [] lines)
    5.99      val n = Logic.count_prems (prop_of goal)
   5.100      val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
   5.101 @@ -559,13 +553,13 @@
   5.102                      ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
   5.103                       space_implode " " xs ^ ")") ^ "."
   5.104  
   5.105 -fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) =
   5.106 +fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
   5.107    let
   5.108      val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
   5.109      val n = Logic.count_prems (prop_of goal)
   5.110      val xs = kill_chained lemmas
   5.111    in
   5.112 -    (metis_line subgoalno n xs ^ minimize_line name xs ^
   5.113 +    (metis_line i n xs ^ minimize_line name xs ^
   5.114       (if used_conj then
   5.115          ""
   5.116        else
   5.117 @@ -573,10 +567,10 @@
   5.118       kill_chained lemmas)
   5.119    end;
   5.120  
   5.121 -fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
   5.122 -                                           goal, subgoalno)) =
   5.123 +fun structured_isar_proof modulus sorts name
   5.124 +        (result as (proof, thm_names, conj_count, ctxt, goal, i)) =
   5.125    let
   5.126 -    (* Could use "split_lines", but it can return blank lines *)
   5.127 +    (* We could use "split_lines", but it can return blank lines. *)
   5.128      val lines = String.tokens (equal #"\n");
   5.129      val kill_spaces =
   5.130        String.translate (fn c => if Char.isSpace c then "" else str c)
   5.131 @@ -586,10 +580,12 @@
   5.132      val tokens = String.tokens (fn c => c = #" ") one_line_proof
   5.133      val isar_proof =
   5.134        if member (op =) tokens chained_hint then ""
   5.135 -      else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
   5.136 +      else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names
   5.137    in
   5.138 -    (one_line_proof ^ "\nStructured proof:\n" ^
   5.139 -     Markup.markup Markup.sendback isar_proof, lemma_names)
   5.140 +    (one_line_proof ^
   5.141 +     (if isar_proof = "" then ""
   5.142 +      else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof),
   5.143 +     lemma_names)
   5.144    end
   5.145  
   5.146  end;