--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 14 16:50:05 2011 +0200
@@ -10,6 +10,7 @@
val keepK = "keep"
val type_encK = "type_enc"
val slicingK = "slicing"
+val lambda_translationK = "lambda_translation"
val e_weight_methodK = "e_weight_method"
val spass_force_sosK = "spass_force_sos"
val vampire_force_sosK = "vampire_force_sos"
@@ -353,8 +354,9 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
- vampire_force_sos hard_timeout timeout dir st =
+fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+ e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
+ st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -367,6 +369,8 @@
val st' =
st |> Proof.map_context
(change_dir dir
+ #> (Option.map (Config.put ATP_Translate.lambda_translation)
+ lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.spass_force_sos)
@@ -455,6 +459,7 @@
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
+ val lambda_translation = AList.lookup (op =) args lambda_translationK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val spass_force_sos = AList.lookup (op =) args spass_force_sosK
|> Option.map (curry (op <>) "false")
@@ -466,8 +471,9 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc max_relevant slicing e_weight_method spass_force_sos
- vampire_force_sos hard_timeout timeout dir st
+ run_sh prover_name prover type_enc max_relevant slicing lambda_translation
+ e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
+ dir st
in
case result of
SH_OK (time_isa, time_prover, names) =>