# HG changeset patch
# User sultana
# Date 1331125230 0
# Node ID 4c80c4034f1d36cc82d892b06db93b677240bdb3
# Parent  98300d5f9cc0792c63c82bddc77471af7690ea11
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;

diff -r 98300d5f9cc0 -r 4c80c4034f1d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 07 13:00:30 2012 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 07 13:00:30 2012 +0000
@@ -23,6 +23,8 @@
 val reconstructorK = "reconstructor"
 val preplay_timeoutK = "preplay_timeout"
 val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*)
+val max_new_mono_instancesK = "max_new_mono_instances"
+val max_mono_itersK = "max_mono_iters"
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -32,6 +34,16 @@
 val separator = "-----"
 
 val preplay_timeout_default = "4"
+(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
+
+(*If a key is present in args then augment a list with its pair*)
+(*This is used to avoid fixing default values at the Mirabelle level, and
+  instead use the default values of the tool (Sledgehammer in this case).*)
+fun available_parameter args key label list =
+  let
+    val value = AList.lookup (op =) args key
+  in if is_some value then (label, the value) :: list else list end
+
 
 datatype sh_data = ShData of {
   calls: int,
@@ -365,7 +377,8 @@
 
 fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
         uncurried_aliases e_weight_method force_sos hard_timeout timeout
-        preplay_timeout sh_minimize dir pos st =
+        preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST
+        dir pos st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -386,7 +399,7 @@
                        force_sos |> the_default I))
     val params as {relevance_thresholds, max_relevant, slice, ...} =
       Sledgehammer_Isar.default_params ctxt
-          [("verbose", "true"),
+         ([("verbose", "true"),
            ("type_enc", type_enc),
            ("strict", strict),
            ("lam_trans", lam_trans |> the_default "smart"),
@@ -394,8 +407,10 @@
            ("max_relevant", max_relevant),
            ("slice", slice),
            ("timeout", string_of_int timeout),
-           ("minimize", sh_minimize), (*don't confuse the two minimization flags*)
            ("preplay_timeout", preplay_timeout)]
+          |> sh_minimizeLST (*don't confuse the two minimization flags*)
+          |> max_new_mono_instancesLST
+          |> max_mono_itersLST)
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
         prover_name
@@ -485,12 +500,16 @@
        minimizer has a chance to do its magic *)
     val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
       |> the_default preplay_timeout_default
-    val sh_minimize = AList.lookup (op =) args sh_minimizeK |> the_default "smart"
+    val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
+    val max_new_mono_instancesLST =
+      available_parameter args max_new_mono_instancesK max_new_mono_instancesK
+    val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_enc strict max_relevant slice lam_trans
         uncurried_aliases e_weight_method force_sos hard_timeout timeout
-        preplay_timeout sh_minimize dir pos st
+        preplay_timeout sh_minimizeLST max_new_mono_instancesLST max_mono_itersLST
+        dir pos st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
@@ -533,15 +552,20 @@
       |> the_default 5
     val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
       |> the_default preplay_timeout_default
-    val sh_minimize = AList.lookup (op =) args sh_minimizeK |> the_default "smart"
+    val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
+    val max_new_mono_instancesLST =
+      available_parameter args max_new_mono_instancesK max_new_mono_instancesK
+    val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
     val params = Sledgehammer_Isar.default_params ctxt
-      [("provers", prover_name),
+     ([("provers", prover_name),
        ("verbose", "true"),
        ("type_enc", type_enc),
        ("strict", strict),
        ("timeout", string_of_int timeout),
-       ("preplay_timeout", preplay_timeout),
-       ("minimize", sh_minimize)] (*don't confuse the two minimization flags*)
+       ("preplay_timeout", preplay_timeout)]
+      |> sh_minimizeLST (*don't confuse the two minimization flags*)
+      |> max_new_mono_instancesLST
+      |> max_mono_itersLST)
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)