# HG changeset patch # User blanchet # Date 1369406617 -7200 # Node ID ac7830871177aa1e76a7c833f4a9999e7e56db6d # Parent c54170ee898b0add8d83e2b4d356d16e9532e25f improved handling of free variables' types in Isar proofs diff -r c54170ee898b -r ac7830871177 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/TPTP/mash_eval.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/TPTP/mash_export.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/TPTP/sledgehammer_tactics.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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)) diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/ATP/atp_util.ML --- 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; diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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) = diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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) diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 = diff -r c54170ee898b -r ac7830871177 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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