--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:20:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 09:42:27 2011 +0100
@@ -11,7 +11,7 @@
val type_encK = "type_enc"
val soundK = "sound"
val slicingK = "slicing"
-val lambda_transK = "lambda_trans"
+val lam_transK = "lam_trans"
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
@@ -355,7 +355,7 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
e_weight_method force_sos hard_timeout timeout dir pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
@@ -371,9 +371,6 @@
val st' =
st |> Proof.map_context
(set_file_name dir
- #> (Option.map (Config.put
- Sledgehammer_Provers.atp_lambda_trans)
- lambda_trans |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
@@ -383,6 +380,7 @@
[("verbose", "true"),
("type_enc", type_enc),
("sound", sound),
+ ("lam_trans", lam_trans |> the_default "smart"),
("preplay_timeout", preplay_timeout),
("max_relevant", max_relevant),
("slicing", slicing),
@@ -465,7 +463,7 @@
val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
- val lambda_trans = AList.lookup (op =) args lambda_transK
+ val lam_trans = AList.lookup (op =) args lam_transK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
@@ -475,7 +473,7 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+ run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
e_weight_method force_sos hard_timeout timeout dir pos st
in
case result of
@@ -576,15 +574,17 @@
ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
- ORELSE' Metis_Tactic.metis_tac [] ctxt thms
+ ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
+ Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc]
+ ATP_Translate.combinatorsN ctxt thms
else if !reconstructor = "metis (no_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
+ Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
+ ATP_Translate.combinatorsN ctxt thms
else if !reconstructor = "metis" then
- Metis_Tactic.metis_tac [] ctxt thms
+ Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
else
K all_tac
end