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

     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 11:16:51 2011 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Mar 31 11:16:52 2011 +0200
     2.3 @@ -555,6 +555,19 @@
     2.4  filter. If the option is set to \textit{smart}, it is set to a value that was
     2.5  empirically found to be appropriate for the prover. A typical value would be
     2.6  300.
     2.7 +
     2.8 +\opfalse{monomorphize}{dont\_monomorphize}
     2.9 +Specifies whether the relevant facts should be monomorphized---i.e., whether
    2.10 +their type variables should be instantiated with relevant ground types.
    2.11 +Monomorphization is always performed for SMT solvers, irrespective of this
    2.12 +option. Monomorphization can simplify reasoning but also leads to larger fact
    2.13 +bases, which can slow down the ATPs.
    2.14 +
    2.15 +\opdefault{monomorphize\_limit}{int}{\upshape 4}
    2.16 +Specifies the maximum number of iterations for the monomorphization fixpoint
    2.17 +construction. The higher this limit is, the more monomorphic instances are
    2.18 +potentially generated.
    2.19 +
    2.20  \end{enum}
    2.21  
    2.22  \subsection{Output Format}

     3.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:51 2011 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:52 2011 +0200
     3.3 @@ -28,8 +28,8 @@
     3.4  
     3.5  signature SMT_MONOMORPH =
     3.6  sig
     3.7 -  val monomorph: (int * thm) list -> Proof.context ->
     3.8 -    (int * thm) list * Proof.context
     3.9 +  val monomorph: ('a * thm) list -> Proof.context ->
    3.10 +    ('a * thm) list * Proof.context
    3.11  end
    3.12  
    3.13  structure SMT_Monomorph: SMT_MONOMORPH =

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 11:16:51 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Mar 31 11:16:52 2011 +0200
     4.3 @@ -88,6 +88,8 @@
     4.4    #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
     4.5    #> fst
     4.6  
     4.7 +val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
     4.8 +
     4.9  fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
    4.10    if String.isSubstring set_ClauseFormulaRelationN output then
    4.11      let
    4.12 @@ -100,7 +102,8 @@
    4.13          |> map (fn s => find_index (curry (op =) s) seq + 1)
    4.14        fun names_for_number j =
    4.15          j |> AList.lookup (op =) name_map |> these
    4.16 -          |> map_filter (try (unprefix fact_prefix)) |> map unascii_of
    4.17 +          |> map_filter (try (unascii_of o unprefix_fact_number
    4.18 +                              o unprefix fact_prefix))
    4.19            |> map (fn name =>
    4.20                       (name, name |> find_first_in_list_vector fact_names |> the)
    4.21                       handle Option.Option =>
    4.22 @@ -145,16 +148,19 @@
    4.23        "\nTo minimize the number of lemmas, try this: " ^
    4.24        Markup.markup Markup.sendback command ^ "."
    4.25  
    4.26 -val vampire_fact_prefix = "f" (* grrr... *)
    4.27 +val vampire_step_prefix = "f" (* grrr... *)
    4.28  
    4.29  fun resolve_fact fact_names ((_, SOME s)) =
    4.30 -    (case strip_prefix_and_unascii fact_prefix s of
    4.31 -       SOME s' => (case find_first_in_list_vector fact_names s' of
    4.32 -                     SOME x => [(s', x)]
    4.33 -                   | NONE => [])
    4.34 +    (case try (unprefix fact_prefix) s of
    4.35 +       SOME s' =>
    4.36 +       let val s' = s' |> unprefix_fact_number |> unascii_of in
    4.37 +         case find_first_in_list_vector fact_names s' of
    4.38 +           SOME x => [(s', x)]
    4.39 +         | NONE => []
    4.40 +       end
    4.41       | NONE => [])
    4.42    | resolve_fact fact_names (num, NONE) =
    4.43 -    case Int.fromString (perhaps (try (unprefix vampire_fact_prefix)) num) of
    4.44 +    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
    4.45        SOME j =>
    4.46        if j > 0 andalso j <= Vector.length fact_names then
    4.47          Vector.sub (fact_names, j - 1)
    4.48 @@ -233,7 +239,7 @@
    4.49  
    4.50  val raw_prefix = "X"
    4.51  val assum_prefix = "A"
    4.52 -val fact_prefix = "F"
    4.53 +val have_prefix = "F"
    4.54  
    4.55  fun resolve_conjecture conjecture_shape (num, s_opt) =
    4.56    let
    4.57 @@ -847,7 +853,7 @@
    4.58                (l, subst, next_fact)
    4.59              else
    4.60                let
    4.61 -                val l' = (prefix_for_depth depth fact_prefix, next_fact)
    4.62 +                val l' = (prefix_for_depth depth have_prefix, next_fact)
    4.63                in (l', (l, l') :: subst, next_fact + 1) end
    4.64            val relabel_facts =
    4.65              apfst (maps (the_list o AList.lookup (op =) subst))

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 11:16:51 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 31 11:16:52 2011 +0200
     5.3 @@ -442,9 +442,13 @@
     5.4                  (atp_type_literals_for_types type_sys ctypes_sorts))
     5.5             (formula_for_combformula ctxt type_sys combformula)
     5.6  
     5.7 -fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
     5.8 -  Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
     5.9 -       NONE)
    5.10 +(* Each fact is given a unique fact number to avoid name clashes (e.g., because
    5.11 +   of monomorphization). The TPTP explicitly forbids name clashes, and some of
    5.12 +   the remote provers might care. *)
    5.13 +fun problem_line_for_fact ctxt prefix type_sys
    5.14 +                          (j, formula as {name, kind, ...}) =
    5.15 +  Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
    5.16 +       formula_for_fact ctxt type_sys formula, NONE)
    5.17  
    5.18  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
    5.19                                                         superclass, ...}) =
    5.20 @@ -626,7 +630,8 @@
    5.21      (* Reordering these might or might not confuse the proof reconstruction
    5.22         code or the SPASS Flotter hack. *)
    5.23      val problem =
    5.24 -      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) facts),
    5.25 +      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
    5.26 +                    (0 upto length facts - 1 ~~ facts)),
    5.27         (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
    5.28         (aritiesN, map problem_line_for_arity_clause arity_clauses),
    5.29         (helpersN, []),
    5.30 @@ -638,7 +643,8 @@
    5.31      val helper_lines =
    5.32        get_helper_facts ctxt explicit_forall type_sys
    5.33                         (maps (map (#3 o dest_Fof) o snd) problem)
    5.34 -      |>> map (problem_line_for_fact ctxt helper_prefix type_sys
    5.35 +      |>> map (pair 0
    5.36 +               #> problem_line_for_fact ctxt helper_prefix type_sys
    5.37                 #> repair_problem_line thy explicit_forall type_sys const_tab)
    5.38        |> op @
    5.39      val (problem, pool) =

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 11:16:51 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 31 11:16:52 2011 +0200
     6.3 @@ -79,10 +79,12 @@
     6.4     ("verbose", "false"),
     6.5     ("overlord", "false"),
     6.6     ("blocking", "false"),
     6.7 +   ("relevance_thresholds", "0.45 0.85"),
     6.8 +   ("max_relevant", "smart"),
     6.9 +   ("monomorphize", "false"),
    6.10 +   ("monomorphize_limit", "4"),
    6.11     ("type_sys", "smart"),
    6.12     ("explicit_apply", "false"),
    6.13 -   ("relevance_thresholds", "0.45 0.85"),
    6.14 -   ("max_relevant", "smart"),
    6.15     ("isar_proof", "false"),
    6.16     ("isar_shrink_factor", "1")]
    6.17  
    6.18 @@ -95,6 +97,7 @@
    6.19     ("quiet", "verbose"),
    6.20     ("no_overlord", "overlord"),
    6.21     ("non_blocking", "blocking"),
    6.22 +   ("dont_monomorphize", "monomorphize"),
    6.23     ("partial_types", "full_types"),
    6.24     ("implicit_apply", "explicit_apply"),
    6.25     ("no_isar_proof", "isar_proof")]
    6.26 @@ -233,6 +236,10 @@
    6.27      val blocking = auto orelse debug orelse lookup_bool "blocking"
    6.28      val provers = lookup_string "provers" |> space_explode " "
    6.29                    |> auto ? single o hd
    6.30 +    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    6.31 +    val max_relevant = lookup_int_option "max_relevant"
    6.32 +    val monomorphize = lookup_bool "monomorphize"
    6.33 +    val monomorphize_limit = lookup_int "monomorphize_limit"
    6.34      val type_sys =
    6.35        case (lookup_string "type_sys", lookup_bool "full_types") of
    6.36          ("tags", full_types) => Tags full_types
    6.37 @@ -245,18 +252,18 @@
    6.38          else
    6.39            error ("Unknown type system: " ^ quote type_sys ^ ".")
    6.40      val explicit_apply = lookup_bool "explicit_apply"
    6.41 -    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    6.42 -    val max_relevant = lookup_int_option "max_relevant"
    6.43      val isar_proof = lookup_bool "isar_proof"
    6.44      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    6.45      val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    6.46      val expect = lookup_string "expect"
    6.47    in
    6.48      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    6.49 -     provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    6.50 -     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    6.51 -     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    6.52 -     timeout = timeout, expect = expect}
    6.53 +     provers = provers, relevance_thresholds = relevance_thresholds,
    6.54 +     max_relevant = max_relevant, monomorphize = monomorphize,
    6.55 +     monomorphize_limit = monomorphize_limit, type_sys = type_sys,
    6.56 +     explicit_apply = explicit_apply, isar_proof = isar_proof,
    6.57 +     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
    6.58 +     expect = expect}
    6.59    end
    6.60  
    6.61  fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 11:16:51 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Mar 31 11:16:52 2011 +0200
     7.3 @@ -42,8 +42,8 @@
     7.4  
     7.5  fun print silent f = if silent then () else Output.urgent_message (f ())
     7.6  
     7.7 -fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
     7.8 -                 isar_shrink_factor, ...} : params)
     7.9 +fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit,
    7.10 +                 type_sys, isar_proof, isar_shrink_factor, ...} : params)
    7.11          explicit_apply_opt silent (prover : prover) timeout i n state facts =
    7.12    let
    7.13      val thy = Proof.theory_of state
    7.14 @@ -65,6 +65,7 @@
    7.15        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    7.16         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    7.17         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    7.18 +       monomorphize = false, monomorphize_limit = monomorphize_limit,
    7.19         isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    7.20         timeout = timeout, expect = ""}
    7.21      val facts =

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:51 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:52 2011 +0200
     8.3 @@ -21,10 +21,12 @@
     8.4       overlord: bool,
     8.5       blocking: bool,
     8.6       provers: string list,
     8.7 +     relevance_thresholds: real * real,
     8.8 +     max_relevant: int option,
     8.9 +     monomorphize: bool,
    8.10 +     monomorphize_limit: int,
    8.11       type_sys: type_system,
    8.12       explicit_apply: bool,
    8.13 -     relevance_thresholds: real * real,
    8.14 -     max_relevant: int option,
    8.15       isar_proof: bool,
    8.16       isar_shrink_factor: int,
    8.17       timeout: Time.time,
    8.18 @@ -66,7 +68,6 @@
    8.19    val smt_iter_fact_frac : real Unsynchronized.ref
    8.20    val smt_iter_time_frac : real Unsynchronized.ref
    8.21    val smt_iter_min_msecs : int Unsynchronized.ref
    8.22 -  val smt_monomorphize_limit : int Unsynchronized.ref
    8.23  
    8.24    val das_Tool : string
    8.25    val select_smt_solver : string -> Proof.context -> Proof.context
    8.26 @@ -229,10 +230,12 @@
    8.27     overlord: bool,
    8.28     blocking: bool,
    8.29     provers: string list,
    8.30 +   relevance_thresholds: real * real,
    8.31 +   max_relevant: int option,
    8.32 +   monomorphize: bool,
    8.33 +   monomorphize_limit: int,
    8.34     type_sys: type_system,
    8.35     explicit_apply: bool,
    8.36 -   relevance_thresholds: real * real,
    8.37 -   max_relevant: int option,
    8.38     isar_proof: bool,
    8.39     isar_shrink_factor: int,
    8.40     timeout: Time.time,
    8.41 @@ -333,13 +336,27 @@
    8.42          ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
    8.43            known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
    8.44            : atp_config)
    8.45 -        ({debug, verbose, overlord, type_sys, explicit_apply, isar_proof,
    8.46 -          isar_shrink_factor, timeout, ...} : params)
    8.47 +        ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys,
    8.48 +          explicit_apply, isar_proof, isar_shrink_factor, timeout, ...}
    8.49 +         : params)
    8.50          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    8.51    let
    8.52      val ctxt = Proof.context_of state
    8.53      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    8.54 -    val facts = facts |> map (atp_translated_fact ctxt)
    8.55 +    fun monomorphize_facts facts =
    8.56 +      let
    8.57 +        val facts = facts |> map untranslated_fact
    8.58 +        val indexed_facts =
    8.59 +          (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts)
    8.60 +      in
    8.61 +        ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
    8.62 +             |> SMT_Monomorph.monomorph indexed_facts |> fst
    8.63 +             |> sort (int_ord o pairself fst)
    8.64 +             |> filter_out (curry (op =) ~1 o fst)
    8.65 +             |> map (Untranslated_Fact o apfst (fst o nth facts))
    8.66 +      end
    8.67 +    val facts = facts |> monomorphize ? monomorphize_facts
    8.68 +                      |> map (atp_translated_fact ctxt)
    8.69      val (dest_dir, problem_prefix) =
    8.70        if overlord then overlord_file_location_for_prover name
    8.71        else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
    8.72 @@ -513,9 +530,9 @@
    8.73  val smt_iter_fact_frac = Unsynchronized.ref 0.5
    8.74  val smt_iter_time_frac = Unsynchronized.ref 0.5
    8.75  val smt_iter_min_msecs = Unsynchronized.ref 5000
    8.76 -val smt_monomorphize_limit = Unsynchronized.ref 4
    8.77  
    8.78 -fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
    8.79 +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
    8.80 +                           timeout, ...} : params)
    8.81                      state i smt_filter =
    8.82    let
    8.83      val ctxt = Proof.context_of state
    8.84 @@ -529,7 +546,7 @@
    8.85            else
    8.86              I)
    8.87        #> Config.put SMT_Config.infer_triggers (!smt_triggers)
    8.88 -      #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit)
    8.89 +      #> Config.put SMT_Config.monomorph_limit monomorphize_limit
    8.90      val state = state |> Proof.map_context repair_context
    8.91  
    8.92      fun iter timeout iter_num outcome0 time_so_far facts =

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 11:16:51 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 31 11:16:52 2011 +0200
     9.3 @@ -164,9 +164,9 @@
     9.4  (* FUDGE *)
     9.5  val auto_max_relevant_divisor = 2
     9.6  
     9.7 -fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
     9.8 -                                 relevance_thresholds, max_relevant, timeout,
     9.9 -                                 ...})
    9.10 +fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
    9.11 +                                 type_sys, relevance_thresholds, max_relevant,
    9.12 +                                 timeout, ...})
    9.13                       auto i (relevance_override as {only, ...}) minimize_command
    9.14                       state =
    9.15    if null provers then
    9.16 @@ -246,7 +246,10 @@
    9.17          else
    9.18            launch_provers state
    9.19                (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
    9.20 -              (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
    9.21 +              (if monomorphize then
    9.22 +                 K (Untranslated_Fact o fst)
    9.23 +               else
    9.24 +                 ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
    9.25                (K (K NONE)) atps
    9.26        fun launch_smts accum =
    9.27          if null smts then