diff -r 1c6031e5d284 -r 4dd63cf5bba5 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 10:45:23 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 10:54:13 2013 +0100 @@ -156,23 +156,22 @@ val leo2_unfold_def_rule = "unfold_def" fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) = - (if rule = leo2_extcnf_equal_neg_rule then - insert (op =) (ext_name ctxt, (Global, General)) - else if rule = leo2_unfold_def_rule then - (* LEO 1.3.3 does not record definitions properly, leading to missing - dependencies in the TSTP proof. Remove the next line once this is - fixed. *) - add_non_rec_defs fact_names - else if rule = satallax_coreN then - (fn [] => - (* Satallax doesn't include definitions in its unsatisfiable cores, - so we assume the worst and include them all here. *) - [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names - | facts => facts) - else - I) - #> (if null deps then union (op =) (resolve_fact fact_names ss) else I) - | add_fact _ _ _ = I + (if rule = leo2_extcnf_equal_neg_rule then + insert (op =) (ext_name ctxt, (Global, General)) + else if rule = leo2_unfold_def_rule then + (* LEO 1.3.3 does not record definitions properly, leading to missing + dependencies in the TSTP proof. Remove the next line once this is + fixed. *) + add_non_rec_defs fact_names + else if rule = satallax_coreN then + (fn [] => + (* Satallax doesn't include definitions in its unsatisfiable cores, so + we assume the worst and include them all here. *) + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names + | facts => facts) + else + I) + #> (if null deps then union (op =) (resolve_fact fact_names ss) else I) fun used_facts_in_atp_proof ctxt fact_names atp_proof = if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names @@ -299,9 +298,6 @@ else s -fun unvarify_term (Var ((s, 0), T)) = Free (s, T) - | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t]) - fun infer_formula_types ctxt = Type.constraint HOLogic.boolT #> Syntax.check_term @@ -326,38 +322,21 @@ | aux t = t in aux end -fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt = - let - val thy = Proof_Context.theory_of ctxt - val t1 = prop_from_atp ctxt true sym_tab phi1 - val vars = snd (strip_comb t1) - val frees = map unvarify_term vars - val unvarify_args = subst_atomic (vars ~~ frees) - val t2 = prop_from_atp ctxt true sym_tab phi2 - val (t1, t2) = - HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt - |> HOLogic.dest_eq - in - (Definition_Step (name, t1, t2), - fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt) - end - | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt = - let - val thy = Proof_Context.theory_of ctxt - val t = u |> prop_from_atp ctxt true sym_tab - |> uncombine_term thy |> infer_formula_types ctxt - in - (Inference_Step (name, role, t, rule, deps), - fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) - end +fun decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt = + let + val thy = Proof_Context.theory_of ctxt + val t = u |> prop_from_atp ctxt true sym_tab + |> uncombine_term thy |> infer_formula_types ctxt + in + (Inference_Step (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) fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] -fun replace_dependencies_in_line _ (line as Definition_Step _) = line - | replace_dependencies_in_line p +fun replace_dependencies_in_line p (Inference_Step (name, role, t, rule, deps)) = Inference_Step (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps []) @@ -368,14 +347,12 @@ fun s_maybe_not role = role <> Conjecture ? s_not -fun is_same_inference _ (Definition_Step _) = false - | is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) = +fun is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) = s_maybe_not role t aconv s_maybe_not role' t' (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) -fun add_line _ (line as Definition_Step _) lines = line :: lines - | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, [])) +fun add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, [])) lines = (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) @@ -389,7 +366,7 @@ lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines = + | add_line _ (line as Inference_Step (name, role, t, _, _)) lines = (* Type information will be deleted later; skip repetition test. *) if is_only_type_information t then line :: lines @@ -406,12 +383,10 @@ let fun do_tail (Inference_Step (name, _, t, rule, deps)) = Inference_Step (name, Negated_Conjecture, s_not t, rule, deps) - | do_tail line = line fun do_body [] = [] | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) = if num = waldmeister_conjecture_num then map do_tail (line :: lines) else line :: do_body lines - | do_body (line :: lines) = line :: do_body lines in do_body end (* Recursively delete empty lines (type information) from the proof. *) @@ -434,25 +409,23 @@ val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule] -fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = - (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line fact_names frees +fun add_desired_line fact_names frees (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) = - (j + 1, - if is_fact fact_names ss orelse - is_conjecture ss orelse - is_skolemize_rule rule orelse - (* the last line must be kept *) - 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 - Inference_Step (name, role, t, rule, deps) :: lines (* keep line *) - else - map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) + (j + 1, + if is_fact fact_names ss orelse + is_conjecture ss orelse + is_skolemize_rule rule orelse + (* the last line must be kept *) + 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 + Inference_Step (name, role, t, rule, deps) :: lines (* keep line *) + else + map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) val indent_size = 2 @@ -709,9 +682,8 @@ else SOME (raw_label_for_name name, nth hyp_ts j) | _ => NONE) | _ => NONE) - fun dep_of_step (Definition_Step _) = NONE - | dep_of_step (Inference_Step (name, _, _, _, from)) = - SOME (from, name) + fun dep_of_step (Inference_Step (name, _, _, _, from)) = + SOME (from, name) val refute_graph = atp_proof |> map_filter dep_of_step |> make_refute_graph val axioms = axioms_of_refute_graph refute_graph conjs @@ -720,8 +692,7 @@ val bot = atp_proof |> List.last |> dep_of_step |> the |> snd val steps = Symtab.empty - |> fold (fn Definition_Step _ => I (* FIXME *) - | Inference_Step (name as (s, _), role, t, rule, _) => + |> fold (fn Inference_Step (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then s_maybe_not role