# HG changeset patch
# User sultana
# Date 1334443937 -3600
# Node ID b5873d4ff1e235bd9f13a1d8882c72d3564d0303
# Parent  24d8c9e9dae4ce81cbdae3d4ab9bd0465561f55a
gathered mirabelle_sledgehammer's hardcoded defaults

diff -r 24d8c9e9dae4 -r b5873d4ff1e2 src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Sat Apr 14 23:52:17 2012 +0100
+++ b/src/HOL/Mirabelle/Actions/mirabelle_sledgehammer.ML	Sat Apr 14 23:52:17 2012 +0100
@@ -46,8 +46,18 @@
 
 val separator = "-----"
 
+(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
+(*defaults used in this Mirabelle action*)
 val preplay_timeout_default = "4"
-(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
+val lam_trans_default = "smart"
+val uncurried_aliases_default = "smart"
+val type_enc_default = "smart"
+val strict_default = "false"
+val max_relevant_default = "smart"
+val slice_default = "true"
+val max_calls_default = "10000000"
+val trivial_default = "false"
+val minimize_timeout_default = 5
 
 (*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
@@ -418,8 +428,8 @@
          ([("verbose", "true"),
            ("type_enc", type_enc),
            ("strict", strict),
-           ("lam_trans", lam_trans |> the_default "smart"),
-           ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
+           ("lam_trans", lam_trans |> the_default lam_trans_default),
+           ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default),
            ("max_relevant", max_relevant),
            ("slice", slice),
            ("timeout", string_of_int timeout),
@@ -501,10 +511,10 @@
     val _ = change_data id inc_sh_calls
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
-    val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
-    val strict = AList.lookup (op =) args strictK |> the_default "false"
-    val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
-    val slice = AList.lookup (op =) args sliceK |> the_default "true"
+    val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
+    val strict = AList.lookup (op =) args strictK |> the_default strict_default
+    val max_relevant = AList.lookup (op =) args max_relevantK |> the_default max_relevant_default
+    val slice = AList.lookup (op =) args sliceK |> the_default slice_default
     val lam_trans = AList.lookup (op =) args lam_transK
     val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
     val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
@@ -562,12 +572,12 @@
     val ctxt = Proof.context_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
-    val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
-    val strict = AList.lookup (op =) args strictK |> the_default "false"
+    val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
+    val strict = AList.lookup (op =) args strictK |> the_default strict_default
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
-      |> the_default 5
+      |> the_default minimize_timeout_default
     val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
       |> the_default preplay_timeout_default
     val sh_minimizeLST = available_parameter args sh_minimizeK "minimize"
@@ -700,7 +710,7 @@
     then () else
     let
       val max_calls =
-        AList.lookup (op =) args max_callsK |> the_default "10000000"
+        AList.lookup (op =) args max_callsK |> the_default max_calls_default
         |> Int.fromString |> the
       val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1;
     in
@@ -713,7 +723,7 @@
           val minimize = AList.defined (op =) args minimizeK
           val metis_ft = AList.defined (op =) args metis_ftK
           val trivial =
-            if AList.lookup (op =) args check_trivialK |> the_default "false"
+            if AList.lookup (op =) args check_trivialK |> the_default trivial_default
                             |> Bool.fromString |> the then
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle TimeLimit.TimeOut => false