# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 8938507b205421143d6e9918b4977540706754fb # Parent 77d9915e6a114e04b8e583db0162d908b30eb2b2 move type declarations to the front, for TFF-compliance diff -r 77d9915e6a11 -r 8938507b2054 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 @@ -13,7 +13,7 @@ type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = string list -> string type metis_params = - string * type_system * minimize_command * string proof + string * type_system * minimize_command * string proof * int * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list @@ -23,9 +23,11 @@ string -> int list list -> (string * locality) list vector -> int list list * (string * locality) list vector val used_facts_in_atp_proof : - (string * locality) list vector -> string proof -> (string * locality) list + int -> (string * locality) list vector -> string proof + -> (string * locality) list val is_unsound_proof : - int list list -> (string * locality) list vector -> string proof -> bool + int list list -> int -> (string * locality) list vector -> string proof + -> bool val apply_on_subgoal : string -> int -> int -> string val command_call : string -> string list -> string val try_command_line : string -> string -> string @@ -50,7 +52,7 @@ type minimize_command = string list -> string type metis_params = - string * type_system * minimize_command * string proof + string * type_system * minimize_command * string proof * int * (string * locality) list vector * thm * int type isar_params = string Symtab.table * bool * int * Proof.context * int list list @@ -122,7 +124,7 @@ val vampire_step_prefix = "f" (* grrr... *) -fun resolve_fact fact_names ((_, SOME s)) = +fun resolve_fact _ fact_names ((_, SOME s)) = (case try (unprefix fact_prefix) s of SOME s' => let val s' = s' |> unprefix_fact_number |> unascii_of in @@ -131,13 +133,15 @@ | NONE => [] end | NONE => []) - | resolve_fact fact_names (num, NONE) = + | resolve_fact facts_offset fact_names (num, NONE) = case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of SOME j => - if j > 0 andalso j <= Vector.length fact_names then - Vector.sub (fact_names, j - 1) - else - [] + let val j = j - facts_offset in + if j > 0 andalso j <= Vector.length fact_names then + Vector.sub (fact_names, j - 1) + else + [] + end | NONE => [] fun resolve_conjecture conjecture_shape (num, s_opt) = @@ -150,25 +154,26 @@ | NONE => ~1 in if k >= 0 then [k] else [] end -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape +fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape -fun add_fact fact_names (Inference (name, _, [])) = - append (resolve_fact fact_names name) - | add_fact _ _ = I +fun add_fact facts_offset fact_names (Inference (name, _, [])) = + append (resolve_fact facts_offset fact_names name) + | add_fact _ _ _ = I -fun used_facts_in_atp_proof fact_names atp_proof = +fun used_facts_in_atp_proof facts_offset fact_names atp_proof = if null atp_proof then Vector.foldl (op @) [] fact_names - else fold (add_fact fact_names) atp_proof [] + else fold (add_fact facts_offset fact_names) atp_proof [] fun is_conjecture_referred_to_in_proof conjecture_shape = exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) -fun is_unsound_proof conjecture_shape fact_names = - (not o is_conjecture_referred_to_in_proof conjecture_shape) andf - forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names +fun is_unsound_proof conjecture_shape facts_offset fact_names = + not o is_conjecture_referred_to_in_proof conjecture_shape andf + forall (is_global_locality o snd) + o used_facts_in_atp_proof facts_offset fact_names (** Soft-core proof reconstruction: Metis one-liner **) @@ -206,11 +211,12 @@ List.partition (curry (op =) Chained o snd) #> pairself (sort_distinct (string_ord o pairself fst)) -fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names, - goal, i) = +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, + facts_offset, fact_names, goal, i) = let val (chained_lemmas, other_lemmas) = - split_used_facts (used_facts_in_atp_proof fact_names atp_proof) + atp_proof |> used_facts_in_atp_proof facts_offset fact_names + |> split_used_facts val n = Logic.count_prems (prop_of goal) in (metis_line banner type_sys i n (map fst other_lemmas) ^ @@ -606,20 +612,22 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) -fun add_fact_from_dependency conjecture_shape fact_names name = +fun add_fact_from_dependency conjecture_shape facts_offset fact_names name = if is_fact fact_names name then - apsnd (union (op =) (map fst (resolve_fact fact_names name))) + apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name))) else apfst (insert (op =) (raw_label_for_name conjecture_shape name)) -fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) - | step_for_line conjecture_shape _ _ (Inference (name, t, [])) = +fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) + | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) = Assume (raw_label_for_name conjecture_shape name, t) - | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) = + | step_for_line conjecture_shape facts_offset fact_names j + (Inference (name, t, deps)) = Have (if j = 1 then [Show] else [], raw_label_for_name conjecture_shape name, fold_rev forall_of (map Var (Term.add_vars t [])) t, - ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names) + ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset + fact_names) deps ([], []))) fun repair_name "$true" = "c_True" @@ -633,7 +641,7 @@ s fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor - atp_proof conjecture_shape fact_names params frees = + atp_proof conjecture_shape facts_offset fact_names params frees = let val lines = atp_proof @@ -647,8 +655,8 @@ |> snd in (if null params then [] else [Fix params]) @ - map2 (step_for_line conjecture_shape fact_names) (length lines downto 1) - lines + map2 (step_for_line conjecture_shape facts_offset fact_names) + (length lines downto 1) lines end (* When redirecting proofs, we keep information about the labels seen so far in @@ -939,7 +947,8 @@ in do_proof end fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) = + (metis_params as (_, type_sys, _, atp_proof, facts_offset, fact_names, + goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] @@ -948,8 +957,8 @@ val (one_line_proof, lemma_names) = metis_proof_text metis_params fun isar_proof_for () = case isar_proof_from_atp_proof pool ctxt type_sys tfrees - isar_shrink_factor atp_proof conjecture_shape fact_names params - frees + isar_shrink_factor atp_proof conjecture_shape facts_offset + fact_names params frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof diff -r 77d9915e6a11 -r 8938507b2054 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -33,7 +33,8 @@ val prepare_atp_problem : Proof.context -> bool -> type_system -> bool -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list - -> string problem * string Symtab.table * int * (string * 'a) list vector + -> string problem * string Symtab.table * int * int + * (string * 'a) list vector val atp_problem_weights : string problem -> (string * real) list end; @@ -798,11 +799,11 @@ `I tff_bool_type)) | add_extra_type_decl_lines _ = I +val type_declsN = "Type declarations" val factsN = "Relevant facts" val class_relsN = "Class relationships" val aritiesN = "Arity declarations" val helpersN = "Helper facts" -val type_declsN = "Type declarations" val conjsN = "Conjectures" val free_typesN = "Type variables" @@ -820,12 +821,12 @@ (* Reordering these might confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = - [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) + [(type_declsN, []), + (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) (0 upto length facts - 1 ~~ facts)), (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), (aritiesN, map problem_line_for_arity_clause arity_clauses), (helpersN, []), - (type_declsN, []), (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] val sym_tab = sym_table_for_problem explicit_apply problem @@ -847,11 +848,12 @@ |> op @ val (problem, pool) = problem |> fold (AList.update (op =)) - [(helpersN, helper_lines), (type_declsN, type_decl_lines)] + [(type_declsN, type_decl_lines), (helpersN, helper_lines)] |> nice_atp_problem readable_names in (problem, case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + offset_of_heading_in_problem factsN problem 0, offset_of_heading_in_problem conjsN problem 0, fact_names |> Vector.fromList) end diff -r 77d9915e6a11 -r 8938507b2054 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:24 2011 +0200 @@ -432,7 +432,8 @@ |> Output.urgent_message else () - val (atp_problem, pool, conjecture_offset, fact_names) = + val (atp_problem, pool, conjecture_offset, facts_offset, + fact_names) = prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem @@ -474,8 +475,8 @@ val outcome = case outcome of NONE => if not (is_type_system_sound type_sys) andalso - is_unsound_proof conjecture_shape fact_names - atp_proof then + is_unsound_proof conjecture_shape facts_offset + fact_names atp_proof then SOME UnsoundProof else NONE @@ -484,7 +485,7 @@ else SOME IncompleteUnprovable | _ => outcome in - ((pool, conjecture_shape, fact_names), + ((pool, conjecture_shape, facts_offset, fact_names), (output, msecs, atp_proof, outcome)) end val timer = Timer.startRealTimer () @@ -503,9 +504,10 @@ end | maybe_run_slice _ _ result = result fun maybe_blacklist_facts_and_retry iter blacklist - (result as ((_, _, fact_names), + (result as ((_, _, facts_offset, fact_names), (_, _, atp_proof, SOME UnsoundProof))) = - (case used_facts_in_atp_proof fact_names atp_proof of + (case used_facts_in_atp_proof facts_offset fact_names + atp_proof of [] => result | new_baddies => let val blacklist = new_baddies @ blacklist in @@ -516,7 +518,7 @@ end) | maybe_blacklist_facts_and_retry _ _ result = result in - ((Symtab.empty, [], Vector.fromList []), + ((Symtab.empty, [], 0, Vector.fromList []), ("", SOME 0, [], SOME InternalError)) |> fold (maybe_run_slice []) actual_slices (* The ATP found an unsound proof? Automatically try again @@ -535,7 +537,7 @@ () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output - val ((pool, conjecture_shape, fact_names), + val ((pool, conjecture_shape, facts_offset, fact_names), (output, msecs, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = @@ -556,8 +558,8 @@ "") val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) val metis_params = - (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names, - goal, subgoal) + (proof_banner auto, type_sys, minimize_command, atp_proof, facts_offset, + fact_names, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of NONE =>