--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 15 11:26:29 2010 +0100
@@ -9,6 +9,7 @@
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
val full_typesK = "full_types"
+val type_sysK = "type_sys"
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
val metis_ftK = "metis_ft"
@@ -342,7 +343,7 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover hard_timeout timeout dir st =
+fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val thy = ProofContext.theory_of ctxt
@@ -356,6 +357,7 @@
val params as {type_sys, relevance_thresholds, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
+ ("type_sys", type_sys),
("timeout", Int.toString timeout)]
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
@@ -414,10 +416,12 @@
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_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
val hard_timeout = SOME timeout (* always use a hard timeout *)
- val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
+ val (msg, result) =
+ run_sh prover_name prover type_sys hard_timeout timeout dir st
in
case result of
SH_OK (time_isa, time_prover, names) =>
@@ -453,13 +457,15 @@
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
val (prover_name, _) = get_prover ctxt args
+ val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
- [("verbose", "true"),
- ("provers", prover_name),
+ [("provers", prover_name),
+ ("verbose", "true"),
+ ("type_sys", type_sys),
("timeout", Int.toString timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts params true 1
@@ -533,6 +539,7 @@
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val ctxt = Proof.context_of pre
val (prover_name, _) = get_prover ctxt args
+ val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
val trivial =