# HG changeset patch # User blanchet # Date 1384881112 -3600 # Node ID 77c9460e01b03b612046de9759a4d8ca41e61867 # Parent f625e0e79dd1d4af8a17180071445dd28bedb6d4 simplified old code diff -r f625e0e79dd1 -r 77c9460e01b0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 18:11:52 2013 +0100 @@ -36,10 +36,12 @@ Proof.context -> bool -> int Symtab.table -> (string, string, (string, string) atp_term, string) atp_formula -> term + (* FIXME: eliminate *) val resolve_fact : (string * 'a) list vector -> string list -> (string * 'a) list val resolve_conjecture : string list -> int list val is_fact : (string * 'a) list vector -> string list -> bool val is_conjecture : string list -> bool + val used_facts_in_atp_proof : Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list diff -r f625e0e79dd1 -r 77c9460e01b0 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 19 18:11:52 2013 +0100 @@ -376,7 +376,7 @@ val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) - val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) + val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) diff -r f625e0e79dd1 -r 77c9460e01b0 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 18:11:52 2013 +0100 @@ -47,18 +47,10 @@ open String_Redirect -val assume_prefix = "a" -val have_prefix = "f" -val raw_prefix = "x" +fun raw_label_of_num num = (num, 0) -fun raw_label_of_name (num, ss) = - case resolve_conjecture ss of - [j] => (conjecture_prefix, j) - | _ => (raw_prefix ^ ascii_of num, 0) - -fun label_of_clause [name] = raw_label_of_name name - | label_of_clause c = - (space_implode "___" (map (fst o raw_label_of_name) c), 0) +fun label_of_clause [(num, _)] = raw_label_of_num num + | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) fun add_fact_of_dependencies fact_names (names as [(_, ss)]) = if is_fact fact_names ss then @@ -150,14 +142,17 @@ fun do_label l = if member (op =) used_ls l then l else no_label fun do_assms (Assume assms) = Assume (map (apfst do_label) assms) fun do_step (Prove (qs, xs, l, t, subproofs, by)) = - Prove (qs, xs, do_label l, t, map do_proof subproofs, by) + Prove (qs, xs, do_label l, t, map do_proof subproofs, by) | do_step step = step and do_proof (Proof (fix, assms, steps)) = - Proof (fix, do_assms assms, map do_step steps) + Proof (fix, do_assms assms, map do_step steps) in do_proof proof end fun prefix_of_depth n = replicate_string (n + 1) +val assume_prefix = "a" +val have_prefix = "f" + val relabel_proof = let fun fresh_label depth prefix (old as (l, subst, next)) = @@ -258,11 +253,11 @@ | _ => NONE) val assms = atp_proof |> map_filter - (fn (name as (_, ss), _, _, _, []) => + (fn ((num, ss), _, _, _, []) => (case resolve_conjecture ss of [j] => if j = length hyp_ts then NONE - else SOME (raw_label_of_name name, nth hyp_ts j) + else SOME (raw_label_of_num num, nth hyp_ts j) | _ => NONE) | _ => NONE) val bot = atp_proof |> List.last |> #1 @@ -312,13 +307,11 @@ (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem - fun skolems_of t = - Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev + fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev fun do_steps outer predecessor accum [] = accum |> (if tainted = [] then - cons (Prove (if outer then [Show] else [], - Fix [], no_label, concl_t, [], + cons (Prove (if outer then [Show] else [], Fix [], no_label, concl_t, [], By_Metis ([the predecessor], []))) else I) @@ -327,26 +320,19 @@ let val l = label_of_clause c val t = prop_of_clause c - val by = - By_Metis - (fold (add_fact_of_dependencies fact_names) gamma no_facts) - fun prove sub by = - Prove (maybe_show outer c [], Fix [], l, t, sub, by) - fun do_rest l step = - do_steps outer (SOME l) (step :: accum) infs + val by = By_Metis (fold (add_fact_of_dependencies fact_names) gamma no_facts) + fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by) + fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then case gamma of [g] => - if is_clause_skolemize_rule g andalso - is_clause_tainted g then + if is_clause_skolemize_rule g andalso is_clause_tainted g then let val subproof = - Proof (Fix (skolems_of (prop_of_clause g)), - Assume [], rev accum) + Proof (Fix (skolems_of (prop_of_clause g)), Assume [], rev accum) in - do_steps outer (SOME l) - [prove [subproof] (By_Metis no_facts)] [] + do_steps outer (SOME l) [prove [subproof] (By_Metis no_facts)] [] end else do_rest l (prove [] by) @@ -360,14 +346,13 @@ | do_steps outer predecessor accum (Cases cases :: infs) = let fun do_case (c, infs) = - do_proof false [] [(label_of_clause c, prop_of_clause c)] - infs + do_proof false [] [(label_of_clause c, prop_of_clause c)] infs val c = succedent_of_cases cases val l = label_of_clause c val t = prop_of_clause c val step = - Prove (maybe_show outer c [], Fix [], l, t, - map do_case cases, By_Metis (the_list predecessor, [])) + Prove (maybe_show outer c [], Fix [], l, t, map do_case cases, + By_Metis (the_list predecessor, [])) in do_steps outer (SOME l) (step :: accum) infs end @@ -393,12 +378,10 @@ preplay_timeout) val ((preplay_time, preplay_fail), isar_proof) = isar_proof - |> compress_proof - (if isar_proofs = SOME true then isar_compress else 1000.0) + |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) preplay_interface |> isar_try0 ? try0 preplay_timeout preplay_interface - |> minimize_dependencies_and_remove_unrefed_steps isar_try0 - preplay_interface + |> minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface |> `overall_preplay_stats ||> clean_up_labels_in_proof val isar_text =