added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default

--- a/NEWS	Thu Mar 31 11:16:51 2011 +0200
+++ b/NEWS	Thu Mar 31 11:16:52 2011 +0200
@@ -49,6 +49,7 @@
 * Sledgehammer:
   - sledgehammer available_provers ~> sledgehammer supported_provers
     INCOMPATIBILITY.
+  - Added "monomorphize" and "monomorphize_limit" options.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.

--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 11:16:51 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 11:16:52 2011 +0200
@@ -555,6 +555,19 @@
 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. A typical value would be
 300.
+
+\opfalse{monomorphize}{dont\_monomorphize}
+Specifies whether the relevant facts should be monomorphized---i.e., whether
+their type variables should be instantiated with relevant ground types.
+Monomorphization is always performed for SMT solvers, irrespective of this
+option. Monomorphization can simplify reasoning but also leads to larger fact
+bases, which can slow down the ATPs.
+
+\opdefault{monomorphize\_limit}{int}{\upshape 4}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated.
+
 \end{enum}
 
 \subsection{Output Format}

--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -28,8 +28,8 @@
 
 signature SMT_MONOMORPH =
 sig
-  val monomorph: (int * thm) list -> Proof.context ->
-    (int * thm) list * Proof.context
+  val monomorph: ('a * thm) list -> Proof.context ->
+    ('a * thm) list * Proof.context
 end
 
 structure SMT_Monomorph: SMT_MONOMORPH =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -88,6 +88,8 @@
   #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   #> fst
 
+val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+
 fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
@@ -100,7 +102,8 @@
         |> map (fn s => find_index (curry (op =) s) seq + 1)
       fun names_for_number j =
         j |> AList.lookup (op =) name_map |> these
-          |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
+          |> map_filter (try (unascii_of o unprefix_fact_number
+                              o unprefix fact_prefix))
           |> map (fn name =>
                      (name, name |> find_first_in_list_vector fact_names |> the)
                      handle Option.Option =>
@@ -145,16 +148,19 @@
       "\nTo minimize the number of lemmas, try this: " ^
       Markup.markup Markup.sendback command ^ "."
 
-val vampire_fact_prefix = "f" (* grrr... *)
+val vampire_step_prefix = "f" (* grrr... *)
 
 fun resolve_fact fact_names ((_, SOME s)) =
-    (case strip_prefix_and_unascii fact_prefix s of
-       SOME s' => (case find_first_in_list_vector fact_names s' of
-                     SOME x => [(s', x)]
-                   | NONE => [])
+    (case try (unprefix fact_prefix) s of
+       SOME s' =>
+       let val s' = s' |> unprefix_fact_number |> unascii_of in
+         case find_first_in_list_vector fact_names s' of
+           SOME x => [(s', x)]
+         | NONE => []
+       end
      | NONE => [])
   | resolve_fact fact_names (num, NONE) =
-    case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
+    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
       SOME j =>
       if j > 0 andalso j <= Vector.length fact_names then
         Vector.sub (fact_names, j - 1)
@@ -233,7 +239,7 @@
 
 val raw_prefix = "X"
 val assum_prefix = "A"
-val fact_prefix = "F"
+val have_prefix = "F"
 
 fun resolve_conjecture conjecture_shape (num, s_opt) =
   let
@@ -847,7 +853,7 @@
               (l, subst, next_fact)
             else
               let
-                val l' = (prefix_for_depth depth fact_prefix, next_fact)
+                val l' = (prefix_for_depth depth have_prefix, next_fact)
               in (l', (l, l') :: subst, next_fact + 1) end
           val relabel_facts =
             apfst (maps (the_list o AList.lookup (op =) subst))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -442,9 +442,13 @@
                 (atp_type_literals_for_types type_sys ctypes_sorts))
            (formula_for_combformula ctxt type_sys combformula)
 
-fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
-  Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
-       NONE)
+(* Each fact is given a unique fact number to avoid name clashes (e.g., because
+   of monomorphization). The TPTP explicitly forbids name clashes, and some of
+   the remote provers might care. *)
+fun problem_line_for_fact ctxt prefix type_sys
+                          (j, formula as {name, kind, ...}) =
+  Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
+       formula_for_fact ctxt type_sys formula, NONE)
 
 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
@@ -626,7 +630,8 @@
     (* Reordering these might or might not confuse the proof reconstruction
        code or the SPASS Flotter hack. *)
     val problem =
-      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
+      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
+                    (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map problem_line_for_arity_clause arity_clauses),
        (helpersN, []),
@@ -638,7 +643,8 @@
     val helper_lines =
       get_helper_facts ctxt explicit_forall type_sys
                        (maps (map (#3 o dest_Fof) o snd) problem)
-      |>> map (problem_line_for_fact ctxt helper_prefix type_sys
+      |>> map (pair 0
+               #> problem_line_for_fact ctxt helper_prefix type_sys
                #> repair_problem_line thy explicit_forall type_sys const_tab)
       |> op @
     val (problem, pool) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -79,10 +79,12 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("blocking", "false"),
+   ("relevance_thresholds", "0.45 0.85"),
+   ("max_relevant", "smart"),
+   ("monomorphize", "false"),
+   ("monomorphize_limit", "4"),
    ("type_sys", "smart"),
    ("explicit_apply", "false"),
-   ("relevance_thresholds", "0.45 0.85"),
-   ("max_relevant", "smart"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1")]
 
@@ -95,6 +97,7 @@
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
    ("non_blocking", "blocking"),
+   ("dont_monomorphize", "monomorphize"),
    ("partial_types", "full_types"),
    ("implicit_apply", "explicit_apply"),
    ("no_isar_proof", "isar_proof")]
@@ -233,6 +236,10 @@
     val blocking = auto orelse debug orelse lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
+    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
+    val max_relevant = lookup_int_option "max_relevant"
+    val monomorphize = lookup_bool "monomorphize"
+    val monomorphize_limit = lookup_int "monomorphize_limit"
     val type_sys =
       case (lookup_string "type_sys", lookup_bool "full_types") of
         ("tags", full_types) => Tags full_types
@@ -245,18 +252,18 @@
         else
           error ("Unknown type system: " ^ quote type_sys ^ ".")
     val explicit_apply = lookup_bool "explicit_apply"
-    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
-    val max_relevant = lookup_int_option "max_relevant"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
-     provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
-     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
-     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
-     timeout = timeout, expect = expect}
+     provers = provers, relevance_thresholds = relevance_thresholds,
+     max_relevant = max_relevant, monomorphize = monomorphize,
+     monomorphize_limit = monomorphize_limit, type_sys = type_sys,
+     explicit_apply = explicit_apply, isar_proof = isar_proof,
+     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
+     expect = expect}
   end
 
 fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -42,8 +42,8 @@
 
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
-fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
-                 isar_shrink_factor, ...} : params)
+fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
+                 type_sys, isar_proof, isar_shrink_factor, ...} : params)
         explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
     val thy = Proof.theory_of state
@@ -65,6 +65,7 @@
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+       monomorphize = false, monomorphize_limit = monomorphize_limit,
        isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
        timeout = timeout, expect = ""}
     val facts =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -21,10 +21,12 @@
      overlord: bool,
      blocking: bool,
      provers: string list,
+     relevance_thresholds: real * real,
+     max_relevant: int option,
+     monomorphize: bool,
+     monomorphize_limit: int,
      type_sys: type_system,
      explicit_apply: bool,
-     relevance_thresholds: real * real,
-     max_relevant: int option,
      isar_proof: bool,
      isar_shrink_factor: int,
      timeout: Time.time,
@@ -66,7 +68,6 @@
   val smt_iter_fact_frac : real Unsynchronized.ref
   val smt_iter_time_frac : real Unsynchronized.ref
   val smt_iter_min_msecs : int Unsynchronized.ref
-  val smt_monomorphize_limit : int Unsynchronized.ref
 
   val das_Tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
@@ -229,10 +230,12 @@
    overlord: bool,
    blocking: bool,
    provers: string list,
+   relevance_thresholds: real * real,
+   max_relevant: int option,
+   monomorphize: bool,
+   monomorphize_limit: int,
    type_sys: type_system,
    explicit_apply: bool,
-   relevance_thresholds: real * real,
-   max_relevant: int option,
    isar_proof: bool,
    isar_shrink_factor: int,
    timeout: Time.time,
@@ -333,13 +336,27 @@
         ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
           known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
           : atp_config)
-        ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof,
-          isar_shrink_factor, timeout, ...} : params)
+        ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys,
+          explicit_apply, isar_proof, isar_shrink_factor, timeout, ...}
+         : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
-    val facts = facts |> map (atp_translated_fact ctxt)
+    fun monomorphize_facts facts =
+      let
+        val facts = facts |> map untranslated_fact
+        val indexed_facts =
+          (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts)
+      in
+        ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
+             |> SMT_Monomorph.monomorph indexed_facts |> fst
+             |> sort (int_ord o pairself fst)
+             |> filter_out (curry (op =) ~1 o fst)
+             |> map (Untranslated_Fact o apfst (fst o nth facts))
+      end
+    val facts = facts |> monomorphize ? monomorphize_facts
+                      |> map (atp_translated_fact ctxt)
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_for_prover name
       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
@@ -513,9 +530,9 @@
 val smt_iter_fact_frac = Unsynchronized.ref 0.5
 val smt_iter_time_frac = Unsynchronized.ref 0.5
 val smt_iter_min_msecs = Unsynchronized.ref 5000
-val smt_monomorphize_limit = Unsynchronized.ref 4
 
-fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
+fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
+                           timeout, ...} : params)
                     state i smt_filter =
   let
     val ctxt = Proof.context_of state
@@ -529,7 +546,7 @@
           else
             I)
       #> Config.put SMT_Config.infer_triggers (!smt_triggers)
-      #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit)
+      #> Config.put SMT_Config.monomorph_limit monomorphize_limit
     val state = state |> Proof.map_context repair_context
 
     fun iter timeout iter_num outcome0 time_so_far facts =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 11:16:51 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 11:16:52 2011 +0200
@@ -164,9 +164,9 @@
 (* FUDGE *)
 val auto_max_relevant_divisor = 2
 
-fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
-                                 relevance_thresholds, max_relevant, timeout,
-                                 ...})
+fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
+                                 type_sys, relevance_thresholds, max_relevant,
+                                 timeout, ...})
                      auto i (relevance_override as {only, ...}) minimize_command
                      state =
   if null provers then
@@ -246,7 +246,10 @@
         else
           launch_provers state
               (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
-              (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
+              (if monomorphize then
+                 K (Untranslated_Fact o fst)
+               else
+                 ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
               (K (K NONE)) atps
       fun launch_smts accum =
         if null smts then