# HG changeset patch
# User smolkas
# Date 1373661685 -7200
# Node ID 23393c31c7feebaae9ca358fa32818ac60548e4a
# Parent  564a108d722f4d3cbac17c16dcdecb612973dd41
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases

diff -r 564a108d722f -r 23393c31c7fe src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 22:41:25 2013 +0200
@@ -102,6 +102,8 @@
    ("isar_compress", "10"),
    ("isar_compress_degree", "2"), (* TODO: document; right value?? *)
    ("merge_timeout_slack", "1.2"), (* TODO: document *)
+   ("isar_try0", "true"), (* TODO: document *)
+   ("isar_minimize", "true"), (* TODO: document *)
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "3"),
@@ -123,13 +125,16 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
+   ("dont_try0_isar", "isar_try0"),
+   ("dont_minimize_isar", "isar_minimize"),
    ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
    "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
-(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace? *)
+(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace,
+   isar_try0, isar_minimize? *)
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -313,6 +318,8 @@
     val isar_compress = Real.max (1.0, lookup_real "isar_compress")
     val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
     val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack")
+    val isar_try0 = lookup_bool "isar_try0"
+    val isar_minimize = lookup_bool "isar_minimize"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =
       if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -330,7 +337,8 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
      isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
-     merge_timeout_slack = merge_timeout_slack, slice = slice,
+     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
+     isar_minimize = isar_minimize, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
      preplay_trace = preplay_trace, expect = expect}
   end
diff -r 564a108d722f -r 23393c31c7fe src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 12 22:41:25 2013 +0200
@@ -59,6 +59,7 @@
                  max_new_mono_instances, type_enc, strict, lam_trans,
                  uncurried_aliases, isar_proofs, isar_compress,
                  isar_compress_degree, merge_timeout_slack,
+                 isar_try0, isar_minimize,
                  preplay_timeout, preplay_trace, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -83,6 +84,7 @@
        isar_proofs = isar_proofs, isar_compress = isar_compress,
        isar_compress_degree = isar_compress_degree,
        merge_timeout_slack = merge_timeout_slack,
+       isar_try0 = isar_try0, isar_minimize = isar_minimize,
        slice = false, minimize = SOME false, timeout = timeout,
        preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
        expect = ""}
@@ -255,7 +257,8 @@
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
          fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
-         isar_compress, isar_compress_degree, merge_timeout_slack, slice,
+         isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0,
+         isar_minimize, slice,
          minimize, timeout, preplay_timeout, preplay_trace, expect} : params) =
   let
     fun lookup_override name default_value =
@@ -274,7 +277,8 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
      isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
-     merge_timeout_slack = merge_timeout_slack, slice = slice,
+     merge_timeout_slack = merge_timeout_slack,
+     isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
      preplay_trace = preplay_trace, expect = expect}
   end
diff -r 564a108d722f -r 23393c31c7fe src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 22:41:25 2013 +0200
@@ -10,7 +10,7 @@
   type preplay_interface = Sledgehammer_Preplay.preplay_interface
   type isar_proof = Sledgehammer_Proof.isar_proof
   val minimize_dependencies_and_remove_unrefed_steps :
-    preplay_interface -> isar_proof -> isar_proof
+    bool -> preplay_interface -> isar_proof -> isar_proof
 end
 
 
@@ -50,7 +50,8 @@
       mk_step_lfs_gfs min_lfs min_gfs
     end)
 
-fun minimize_dependencies_and_remove_unrefed_steps preplay_interface proof =
+fun minimize_dependencies_and_remove_unrefed_steps
+  isar_minimize preplay_interface proof =
   let
     fun cons_to xs x = x :: xs
 
@@ -85,7 +86,8 @@
             (refed, accu)
 
     and do_refed_step step =
-      min_deps_of_step preplay_interface step
+      step
+      |> isar_minimize ? min_deps_of_step preplay_interface
       |> do_refed_step'
 
     and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
diff -r 564a108d722f -r 23393c31c7fe src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 12 22:41:25 2013 +0200
@@ -38,6 +38,8 @@
      isar_compress : real,
      isar_compress_degree : int,
      merge_timeout_slack : real,
+     isar_try0 : bool,
+     isar_minimize : bool,
      slice : bool,
      minimize : bool option,
      timeout : Time.time option,
@@ -351,6 +353,8 @@
    isar_compress : real,
    isar_compress_degree : int,
    merge_timeout_slack : real,
+   isar_try0 : bool,
+   isar_minimize : bool,
    slice : bool,
    minimize : bool option,
    timeout : Time.time option,
@@ -684,6 +688,7 @@
                     uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_compress,
                     isar_compress_degree, merge_timeout_slack,
+                    isar_try0, isar_minimize,
                     slice, timeout, preplay_timeout, preplay_trace, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
@@ -959,6 +964,7 @@
                 val isar_params =
                   (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
                    isar_compress_degree, merge_timeout_slack,
+                   isar_try0,isar_minimize,
                    pool, fact_names, lifted, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
diff -r 564a108d722f -r 23393c31c7fe src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 22:41:25 2013 +0200
@@ -12,7 +12,7 @@
   type one_line_params = Sledgehammer_Print.one_line_params
 
   type isar_params =
-    bool * bool * Time.time option * bool * real * int * real
+    bool * bool * Time.time option * bool * real * int * real * bool * bool
     * string Symtab.table * (string * stature) list vector
     * (string * term) list * int Symtab.table * string proof * thm
 
@@ -409,14 +409,14 @@
   in chain_proof end
 
 type isar_params =
-  bool * bool * Time.time option * bool * real * int * real
+  bool * bool * Time.time option * bool * real * int * real * bool * bool
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
-     isar_compress_degree, merge_timeout_slack, pool, fact_names, lifted,
-     sym_tab, atp_proof, goal)
+     isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
+     fact_names, lifted, sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -594,8 +594,9 @@
                (if isar_proofs = SOME true then isar_compress else 1000.0)
                (if isar_proofs = SOME true then isar_compress_degree else 100)
                merge_timeout_slack preplay_interface
-          |> try0 preplay_timeout preplay_interface
-          |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
+          |> isar_try0 ? try0 preplay_timeout preplay_interface
+          |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
+               preplay_interface
           |> `overall_preplay_stats
           ||> clean_up_labels_in_proof
         val isar_text = string_of_proof ctxt type_enc lam_trans subgoal