killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
authorblanchet
Wed, 08 Jun 2011 08:47:43 +0200
changeset 43259 30c141dc22d6
parent 43258 956895f99904
child 43260 7b875e14b90d
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/atp_export.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -131,8 +131,7 @@
   val type_constrs_of_terms : theory -> term list -> string list
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_sys
-    -> bool option -> bool -> bool -> term list -> term
-    -> ((string * locality) * term) list
+    -> bool -> bool -> term list -> term -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
@@ -1833,9 +1832,10 @@
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
 
+val explicit_apply = NONE (* for experimental purposes *)
+
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
-                        explicit_apply readable_names preproc hyp_ts concl_t
-                        facts =
+                        readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_sys) = choose_format [format] type_sys
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -706,7 +706,7 @@
       val ax_counts =
         Int_Tysubst_Table.empty
         |> fold (fn (ax_no, (_, (tysubst, _))) =>
-                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
+                    Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0)
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
       val needed_axiom_props =
--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -167,7 +167,6 @@
 fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
   let
     val type_sys = type_sys_from_string type_sys
-    val explicit_apply = NONE
     val clauses =
       conj_clauses @ fact_clauses
       |> (if polymorphism_of_type_sys type_sys = Polymorphic then
@@ -188,8 +187,8 @@
 val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
 *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
-                          false false props @{prop False} []
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
+                          @{prop False} []
 (*
 val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
 *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -96,7 +96,6 @@
    ("max_relevant", "smart"),
    ("max_mono_iters", "3"),
    ("max_new_mono_instances", "400"),
-   ("explicit_apply", "smart"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
    ("slicing", "true"),
@@ -112,14 +111,13 @@
    ("no_overlord", "overlord"),
    ("non_blocking", "blocking"),
    ("partial_types", "full_types"),
-   ("implicit_apply", "explicit_apply"),
    ("no_isar_proof", "isar_proof"),
    ("no_slicing", "slicing")]
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
-   "max_new_mono_instances", "explicit_apply", "isar_proof",
-   "isar_shrink_factor", "timeout", "preplay_timeout"]
+   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
+   "preplay_timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
 
@@ -284,7 +282,6 @@
     val max_relevant = lookup_option lookup_int "max_relevant"
     val max_mono_iters = lookup_int "max_mono_iters"
     val max_new_mono_instances = lookup_int "max_new_mono_instances"
-    val explicit_apply = lookup_option lookup_bool "explicit_apply"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
@@ -299,9 +296,9 @@
      provers = provers, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
-     explicit_apply = explicit_apply, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+     slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -47,7 +47,7 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
-                 max_new_mono_instances, type_sys, explicit_apply, isar_proof,
+                 max_new_mono_instances, type_sys, isar_proof,
                  isar_shrink_factor, preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -59,7 +59,7 @@
     val {goal, ...} = Proof.goal state
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
-       provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
+       provers = provers, type_sys = type_sys,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
@@ -73,16 +73,18 @@
     val result as {outcome, used_facts, run_time_in_msecs, ...} =
       prover params (K (K "")) problem
   in
-    print silent (fn () =>
-        case outcome of
-          SOME failure => string_for_failure failure
-        | NONE => "Found proof" ^
-                  (if length used_facts = length facts then ""
-                   else " with " ^ n_facts used_facts) ^
-                  (case run_time_in_msecs of
-                     SOME ms =>
-                     " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
-                   | NONE => "") ^ ".");
+    print silent
+          (fn () =>
+              case outcome of
+                SOME failure => string_for_failure failure
+              | NONE =>
+                "Found proof" ^
+                 (if length used_facts = length facts then ""
+                  else " with " ^ n_facts used_facts) ^
+                 (case run_time_in_msecs of
+                    SOME ms =>
+                    " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
+                  | NONE => "") ^ ".");
     result
   end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -33,7 +33,6 @@
      max_relevant: int option,
      max_mono_iters: int,
      max_new_mono_instances: int,
-     explicit_apply: bool option,
      isar_proof: bool,
      isar_shrink_factor: int,
      slicing: bool,
@@ -301,7 +300,6 @@
    max_relevant: int option,
    max_mono_iters: int,
    max_new_mono_instances: int,
-   explicit_apply: bool option,
    isar_proof: bool,
    isar_shrink_factor: int,
    slicing: bool,
@@ -549,8 +547,8 @@
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
         ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters,
-          max_new_mono_instances, explicit_apply, isar_proof,
-          isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
+          max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
+          timeout, preplay_timeout, ...} : params)
         minimize_command
         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
@@ -655,9 +653,8 @@
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_sys explicit_apply
-                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
-                      facts
+                      type_sys (Config.get ctxt atp_readable_names) true hyp_ts
+                      concl_t facts
                 fun weights () = atp_problem_weights atp_problem
                 val core =
                   File.shell_path command ^ " " ^
--- a/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -102,11 +102,10 @@
     val facts =
       facts0 |> map (fn ((_, loc), th) =>
                         ((Thm.get_name_hint th, loc), prop_of th))
-    val explicit_apply = NONE
     val (atp_problem, _, _, _, _, _, _) =
       ATP_Translate.prepare_atp_problem ctxt format
-          ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
-          [] @{prop False} facts
+          ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true []
+          @{prop False} facts
     val infers =
       facts0 |> map (fn (_, th) =>
                         (fact_name_of (Thm.get_name_hint th),