added "modulus" and "sorts" options to control Sledgehammer's Isar proof output

--- a/src/HOL/Sledgehammer.thy	Mon Mar 29 18:44:24 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Mar 29 19:49:57 2010 +0200
@@ -99,7 +99,6 @@
 setup Sledgehammer_Fact_Preprocessor.setup
 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
-setup Sledgehammer_Proof_Reconstruct.setup
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
 use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_wrapper.ML"

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 18:44:24 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 19:49:57 2010 +0200
@@ -21,6 +21,8 @@
      higher_order: bool option,
      follow_defs: bool,
      isar_proof: bool,
+     modulus: int,
+     sorts: bool,
      timeout: Time.time,
      minimize_timeout: Time.time}
   type problem =
@@ -71,6 +73,8 @@
    higher_order: bool option,
    follow_defs: bool,
    isar_proof: bool,
+   modulus: int,
+   sorts: bool,
    timeout: Time.time,
    minimize_timeout: Time.time}
 

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 29 18:44:24 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 29 19:49:57 2010 +0200
@@ -160,7 +160,8 @@
         (name, {command, arguments, failure_strs, max_new_clauses,
                 prefers_theory_const, supports_isar_proofs})
         (params as {respect_no_atp, relevance_threshold, convergence,
-                    theory_const, higher_order, follow_defs, isar_proof, ...})
+                    theory_const, higher_order, follow_defs, isar_proof,
+                    modulus, sorts, ...})
         timeout =
   generic_prover
       (get_relevant_facts respect_no_atp relevance_threshold convergence
@@ -168,8 +169,10 @@
                           (the_default prefers_theory_const theory_const))
       (prepare_clauses higher_order false) write_tptp_file command
       (arguments timeout) failure_strs
-      (if supports_isar_proofs andalso isar_proof then structured_isar_proof
-       else metis_lemma_list false) name params;
+      (if supports_isar_proofs andalso isar_proof then
+         structured_isar_proof modulus sorts
+       else
+         metis_lemma_list false) name params;
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
 
@@ -215,7 +218,7 @@
         (name, ({command, arguments, failure_strs, max_new_clauses,
                  prefers_theory_const, ...} : prover_config))
         (params as {respect_no_atp, relevance_threshold, convergence,
-                    theory_const, higher_order, follow_defs, isar_proof, ...})
+                    theory_const, higher_order, follow_defs, ...})
         timeout =
   generic_prover
       (get_relevant_facts respect_no_atp relevance_threshold convergence

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 18:44:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 19:49:57 2010 +0200
@@ -47,6 +47,8 @@
    ("higher_order", "smart"),
    ("follow_defs", "false"),
    ("isar_proof", "false"),
+   ("modulus", "1"),
+   ("sorts", "false"),
    ("minimize_timeout", "5 s")]
 
 val negated_params =
@@ -57,7 +59,8 @@
    ("no_theory_const", "theory_const"),
    ("first_order", "higher_order"),
    ("dont_follow_defs", "follow_defs"),
-   ("metis_proof", "isar_proof")]
+   ("metis_proof", "isar_proof"),
+   ("no_sorts", "sorts")]
 
 val property_dependent_params = ["atps", "full_types", "timeout"]
 
@@ -130,6 +133,8 @@
     val higher_order = lookup_bool_option "higher_order"
     val follow_defs = lookup_bool "follow_defs"
     val isar_proof = lookup_bool "isar_proof"
+    val modulus = Int.max (1, lookup_int "modulus")
+    val sorts = lookup_bool "sorts"
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
@@ -137,8 +142,8 @@
      respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
      convergence = convergence, theory_const = theory_const,
      higher_order = higher_order, follow_defs = follow_defs,
-     isar_proof = isar_proof, timeout = timeout,
-     minimize_timeout = minimize_timeout}
+     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
+     timeout = timeout, minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 18:44:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 19:49:57 2010 +0200
@@ -12,12 +12,11 @@
   val num_typargs: theory -> string -> int
   val make_tvar: string -> typ
   val strip_prefix: string -> string -> string option
-  val setup: theory -> theory
   val is_proof_well_formed: string -> bool
   val metis_line: int -> int -> string list -> string
   val metis_lemma_list: bool -> string ->
     string * string vector * (int * int) * Proof.context * thm * int -> string * string list
-  val structured_isar_proof: string ->
+  val structured_isar_proof: int -> bool -> string ->
     string * string vector * (int * int) * Proof.context * thm * int -> string * string list
 end;
 
@@ -34,14 +33,6 @@
 
 fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
 
-(*For generating structured proofs: keep every nth proof line*)
-val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1);
-
-(*Indicates whether to include sort information in generated proofs*)
-val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true);
-
-val setup = modulus_setup #> recon_sorts_setup;
-
 (**** PARSING OF TSTP FORMAT ****)
 
 (*Syntax trees, either termlist or formulae*)
@@ -336,10 +327,13 @@
 
 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   ATP may have their literals reordered.*)
-fun isar_proof_body ctxt ctms =
+fun isar_proof_body ctxt sorts ctms =
   let
     val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
-    val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
+    val string_of_term = 
+      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                              (print_mode_value ()))
+                      (Syntax.string_of_term ctxt)
     fun have_or_show "show" _ = "  show \""
       | have_or_show have lname = "  " ^ have ^ " " ^ lname ^ ": \""
     fun do_line _ (lname, t, []) =
@@ -355,7 +349,7 @@
     fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
       | do_lines ((lname, t, deps) :: lines) =
         do_line "have" (lname, t, deps) :: do_lines lines
-  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
+  in setmp_CRITICAL show_sorts sorts do_lines end;
 
 fun unequal t (_, t', _) = not (t aconv t');
 
@@ -405,13 +399,13 @@
   counts the number of proof lines processed so far.
   Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
   phase may delete some dependencies, hence this phase comes later.*)
-fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
+fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) =
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
-  | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
+  | add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) =
       if eq_types t orelse not (null (Term.add_tvars t [])) orelse
          exists_subterm bad_free t orelse
          (not (null lines) andalso   (*final line can't be deleted for these reasons*)
-          (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))
+          (length deps < 2 orelse nlines mod modulus <> 0))
       then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
       else (nlines+1, (lno, t, deps) :: lines);
 
@@ -436,7 +430,7 @@
 fun isar_proof_end 1 = "qed"
   | isar_proof_end _ = "next"
 
-fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names =
+fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names =
   let
     val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
     val tuples = map (dest_tstp o tstp_line o explode) cnfs
@@ -449,7 +443,7 @@
     val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
     val _ = trace_proof_msg (fn () =>
       Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
-    val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
+    val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines
     val _ = trace_proof_msg (fn () =>
       Int.toString (length lines) ^ " lines extracted\n")
     val (ccls, fixes) = neg_conjecture_clauses ctxt goal i
@@ -458,7 +452,7 @@
     val ccls = map forall_intr_vars ccls
     val _ = app (fn th => trace_proof_msg
                               (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
-    val body = isar_proof_body ctxt (map prop_of ccls)
+    val body = isar_proof_body ctxt sorts (map prop_of ccls)
                                (stringify_deps thm_names [] lines)
     val n = Logic.count_prems (prop_of goal)
     val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
@@ -559,13 +553,13 @@
                     ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
                      space_implode " " xs ^ ")") ^ "."
 
-fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) =
+fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
   let
     val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
     val n = Logic.count_prems (prop_of goal)
     val xs = kill_chained lemmas
   in
-    (metis_line subgoalno n xs ^ minimize_line name xs ^
+    (metis_line i n xs ^ minimize_line name xs ^
      (if used_conj then
         ""
       else
@@ -573,10 +567,10 @@
      kill_chained lemmas)
   end;
 
-fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt,
-                                           goal, subgoalno)) =
+fun structured_isar_proof modulus sorts name
+        (result as (proof, thm_names, conj_count, ctxt, goal, i)) =
   let
-    (* Could use "split_lines", but it can return blank lines *)
+    (* We could use "split_lines", but it can return blank lines. *)
     val lines = String.tokens (equal #"\n");
     val kill_spaces =
       String.translate (fn c => if Char.isSpace c then "" else str c)
@@ -586,10 +580,12 @@
     val tokens = String.tokens (fn c => c = #" ") one_line_proof
     val isar_proof =
       if member (op =) tokens chained_hint then ""
-      else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
+      else isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names
   in
-    (one_line_proof ^ "\nStructured proof:\n" ^
-     Markup.markup Markup.sendback isar_proof, lemma_names)
+    (one_line_proof ^
+     (if isar_proof = "" then ""
+      else "\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof),
+     lemma_names)
   end
 
 end;