--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 24 16:43:37 2013 +0200
@@ -454,7 +454,7 @@
Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 24 16:43:37 2013 +0200
@@ -124,7 +124,8 @@
extract_relevance_fudge args
(Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
val subgoal = 1
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
+ val ((_, hyp_ts, concl_t), ctxt) =
+ ATP_Util.strip_subgoal goal subgoal ctxt
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
--- a/src/HOL/TPTP/mash_eval.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri May 24 16:43:37 2013 +0200
@@ -109,7 +109,7 @@
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = isar_dependencies_of name_tabs th
val facts =
facts
--- a/src/HOL/TPTP/mash_export.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri May 24 16:43:37 2013 +0200
@@ -207,7 +207,7 @@
val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = isar_dependencies_of name_tabs th
in
if is_bad_query ctxt ho_atp step j th isar_deps then
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri May 24 16:43:37 2013 +0200
@@ -32,7 +32,7 @@
val name = hd provers
val prover = get_prover ctxt mode name
val default_max_facts = default_max_facts_of_prover ctxt slice name
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
val ho_atp = exists (is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
val css_table = clasimpset_rule_table_of ctxt
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri May 24 16:43:37 2013 +0200
@@ -799,8 +799,8 @@
fun lift_lams_part_2 ctxt (facts, lifted) =
(facts, lifted)
- (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
- of them *)
+ (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
+ get rid of them *)
|> pairself (map (introduce_combinators ctxt))
|> pairself (map constify_lifted)
(* Requires bound variables not to clash with any schematic variables (as
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri May 24 16:43:37 2013 +0200
@@ -148,7 +148,7 @@
(* The number of type arguments of a constant, zero if it's monomorphic. For
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
-fun num_type_args thy s =
+fun robust_const_num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
s |> Long_Name.explode |> List.last |> Int.fromString |> the
else if String.isPrefix lam_lifted_prefix s then
@@ -222,7 +222,7 @@
val term_ts = map (do_term [] NONE) term_us
val T =
(if not (null type_us) andalso
- num_type_args thy s' = length type_us then
+ robust_const_num_type_args thy s' = length type_us then
let val Ts = type_us |> map (typ_of_atp ctxt) in
if new_skolem then
SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
--- a/src/HOL/Tools/ATP/atp_util.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri May 24 16:43:37 2013 +0200
@@ -49,7 +49,8 @@
val transform_elim_prop : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val strip_subgoal :
- Proof.context -> thm -> int -> (string * typ) list * term list * term
+ thm -> int -> Proof.context
+ -> ((string * typ) list * term list * term) * Proof.context
end;
structure ATP_Util : ATP_UTIL =
@@ -429,13 +430,19 @@
| NONE => raise Type.TYPE_MATCH
end
-fun strip_subgoal ctxt goal i =
+fun strip_subgoal goal i ctxt =
let
- val (t, (frees, params)) =
+ val (t, ((frees, params), ctxt)) =
Logic.goal_params (prop_of goal) i
- ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
+ ||> map dest_Free
+ ||> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
+ ||> (fn fixes =>
+ ctxt |> Variable.set_body false
+ |> Proof_Context.add_fixes fixes
+ |>> map2 (fn (_, SOME T, _) => fn s => (s, T)) fixes)
+ ||> apfst (`(map Free))
val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
- in (rev params, hyp_ts, concl_t) end
+ in ((rev params, hyp_ts, concl_t), ctxt) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 24 16:43:37 2013 +0200
@@ -707,7 +707,7 @@
let
val thy = Proof_Context.theory_of ctxt
val goal = goal_of_thm thy th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal 1 ctxt
val facts = facts |> filter (fn (_, th') => thm_less (th', th))
fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
fun is_dep dep (_, th) = nickname_of_thm th = dep
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri May 24 16:43:37 2013 +0200
@@ -92,6 +92,7 @@
end
exception ZEROTIME
+
fun try_metis debug trace type_enc lam_trans ctxt timeout step =
let
val (prop, subproofs, fact_names, obtain) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 24 16:43:37 2013 +0200
@@ -686,7 +686,7 @@
val atp_mode =
if Config.get ctxt completish then Sledgehammer_Completish
else Sledgehammer
- val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
+ val ((_, hyp_ts, concl_t), ctxt') = strip_subgoal goal subgoal ctxt
val (dest_dir, problem_prefix) =
if overlord then overlord_file_location_of_prover name
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri May 24 16:43:37 2013 +0200
@@ -323,17 +323,14 @@
| aux t = t
in aux end
-fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
+fun decode_line ctxt sym_tab (name, role, u, rule, deps) =
let
val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_of_atp ctxt true sym_tab
- |> uncombine_term thy |> infer_formula_types ctxt
- in
- ((name, role, t, rule, deps),
- fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
- end
-fun decode_lines ctxt sym_tab lines =
- fst (fold_map (decode_line sym_tab) lines ctxt)
+ val t =
+ u |> prop_of_atp ctxt true sym_tab
+ |> uncombine_term thy
+ |> infer_formula_types ctxt
+ in (name, role, t, rule, deps) end
fun replace_one_dependency (old, new) dep =
if is_same_atp_step dep old then new else [dep]
@@ -395,18 +392,13 @@
fold_rev add_nontrivial_line
(map (replace_dependencies_in_line (name, [])) lines) []
-(* ATPs sometimes reuse free variable names in the strangest ways. Removing
- offending lines often does the trick. *)
-fun is_bad_free frees (Free x) = not (member (op =) frees x)
- | is_bad_free _ _ = false
-
val e_skolemize_rule = "skolemize"
val vampire_skolemisation_rule = "skolemisation"
val is_skolemize_rule =
member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
-fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps)
+fun add_desired_line fact_names (name as (_, ss), role, t, rule, deps)
(j, lines) =
(j + 1,
if is_fact fact_names ss orelse
@@ -416,7 +408,6 @@
j = 0 orelse
(not (is_only_type_information t) andalso
null (Term.add_tvars t []) andalso
- not (exists_subterm (is_bad_free frees) t) andalso
length deps >= 2 andalso
(* kill next to last line, which usually results in a trivial step *)
j <> 1) then
@@ -643,8 +634,7 @@
fact_names, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
- val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
- val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+ val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt
val one_line_proof = one_line_proof_text 0 one_line_params
val type_enc =
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
@@ -659,12 +649,12 @@
|> clean_up_atp_proof_dependencies
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
- |> decode_lines ctxt sym_tab
+ |> map (decode_line ctxt sym_tab)
|> repair_waldmeister_endgame
|> rpair [] |-> fold_rev (add_line fact_names)
|> rpair [] |-> fold_rev add_nontrivial_line
|> rpair (0, [])
- |-> fold_rev (add_desired_line fact_names frees)
+ |-> fold_rev (add_desired_line fact_names)
|> snd
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
val conjs =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 24 16:43:37 2013 +0200
@@ -198,7 +198,7 @@
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
val {facts = chained, goal, ...} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
+ val ((_, hyp_ts, concl_t), _) = strip_subgoal goal i ctxt
val ho_atp = exists (is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
val css = clasimpset_rule_table_of ctxt