# HG changeset patch
# User blanchet
# Date 1407157322 -7200
# Node ID 2bf99b3f62e101c9e55d85beb228a6f1d57461af
# Parent  b5dc0562c7fbcc3fbe76701c5c8327e5c5d6e85d
cleaner 'compress' option

diff -r b5dc0562c7fb -r 2bf99b3f62e1 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Aug 04 15:02:02 2014 +0200
@@ -91,7 +91,7 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "smart"),
-   ("compress", "10"),
+   ("compress", "smart"),
    ("try0", "true"),
    ("smt_proofs", "smart"),
    ("slice", "true"),
@@ -101,7 +101,7 @@
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),
-   ("dont_compress", ("compress", ["0"])),
+   ("dont_compress", ("compress", ["1"])),
    ("isar_proof", ("isar_proofs", [])) (* legacy *)]
 val negated_alias_params =
   [("no_debug", "debug"),
@@ -291,7 +291,7 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
-    val compress = Real.max (1.0, lookup_real "compress")
+    val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_option lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
diff -r b5dc0562c7fb -r 2bf99b3f62e1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 04 15:02:02 2014 +0200
@@ -16,7 +16,7 @@
   val trace : bool Config.T
 
   type isar_params =
-    bool * (string option * string option) * Time.time * real * bool * bool
+    bool * (string option * string option) * Time.time * real option * bool * bool
     * (term, string) atp_step list * thm
 
   val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
@@ -124,7 +124,7 @@
     end
 
 type isar_params =
-  bool * (string option * string option) * Time.time * real * bool * bool
+  bool * (string option * string option) * Time.time * real option * bool * bool
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
@@ -161,7 +161,10 @@
         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
         val do_preplay = preplay_timeout <> Time.zeroTime
-        val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
+        val compress =
+          (case compress of
+            NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
+          | SOME n => n)
 
         fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
         fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
diff -r b5dc0562c7fb -r 2bf99b3f62e1 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Aug 04 15:02:02 2014 +0200
@@ -35,7 +35,7 @@
      max_mono_iters : int option,
      max_new_mono_instances : int option,
      isar_proofs : bool option,
-     compress : real,
+     compress : real option,
      try0 : bool,
      smt_proofs : bool option,
      slice : bool,
@@ -126,7 +126,7 @@
    max_mono_iters : int option,
    max_new_mono_instances : int option,
    isar_proofs : bool option,
-   compress : real,
+   compress : real option,
    try0 : bool,
    smt_proofs : bool option,
    slice : bool,