# HG changeset patch # User blanchet # Date 1307571388 -7200 # Node ID 6901ebafbb8d0b4f43cc363bb37318f44d064ae4 # Parent c4ea897a53260b3aa0662b972ece950a4a9d4e9c cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices) diff -r c4ea897a5326 -r 6901ebafbb8d src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Jun 09 00:16:28 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Jun 09 00:16:28 2011 +0200 @@ -12,7 +12,6 @@ type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula type 'a proof = 'a ATP_Proof.proof type locality = ATP_Translate.locality - type type_sys = ATP_Translate.type_sys datatype reconstructor = Metis | @@ -29,18 +28,18 @@ type one_line_params = play * string * (string * locality) list * minimize_command * int * int type isar_params = - bool * bool * int * type_sys * string Symtab.table * int list list * int + bool * bool * int * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof * thm val repair_conjecture_shape_and_fact_names : - type_sys -> string -> int list list -> int - -> (string * locality) list vector -> int list + string -> int list list -> int -> (string * locality) list vector + -> int list -> int list list * int * (string * locality) list vector * int list val used_facts_in_atp_proof : - Proof.context -> type_sys -> int -> (string * locality) list vector - -> string proof -> (string * locality) list + Proof.context -> int -> (string * locality) list vector -> string proof + -> (string * locality) list val used_facts_in_unsound_atp_proof : - Proof.context -> type_sys -> int list list -> int - -> (string * locality) list vector -> 'a proof -> string list option + Proof.context -> int list list -> int -> (string * locality) list vector + -> 'a proof -> string list option val uses_typed_helpers : int list -> 'a proof -> bool val one_line_proof_text : one_line_params -> string val make_tvar : string -> typ @@ -80,7 +79,7 @@ type one_line_params = play * string * (string * locality) list * minimize_command * int * int type isar_params = - bool * bool * int * type_sys * string Symtab.table * int list list * int + bool * bool * int * string Symtab.table * int list list * int * (string * locality) list vector * int Symtab.table * string proof * thm fun is_head_digit s = Char.isDigit (String.sub (s, 0)) @@ -122,11 +121,9 @@ #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation #> fst -fun maybe_unprefix_fact_number type_sys = - polymorphism_of_type_sys type_sys <> Polymorphic - ? (space_implode "_" o tl o space_explode "_") +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" -fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape +fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset fact_names typed_helpers = if String.isSubstring set_ClauseFormulaRelationN output then let @@ -139,7 +136,7 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) fun names_for_number j = j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys + |> map_filter (try (unascii_of o unprefix_fact_number o unprefix fact_prefix)) |> map (fn name => (name, name |> find_first_in_list_vector fact_names |> the) @@ -158,16 +155,16 @@ val extract_step_number = Int.fromString o perhaps (try (unprefix vampire_step_prefix)) -fun resolve_fact type_sys _ fact_names (_, SOME s) = +fun resolve_fact _ fact_names (_, SOME s) = (case try (unprefix fact_prefix) s of SOME s' => - let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in + let val s' = s' |> unprefix_fact_number |> unascii_of in case find_first_in_list_vector fact_names s' of SOME x => [(s', x)] | NONE => [] end | NONE => []) - | resolve_fact _ facts_offset fact_names (num, NONE) = + | resolve_fact facts_offset fact_names (num, NONE) = (case extract_step_number num of SOME j => let val j = j - facts_offset in @@ -178,8 +175,7 @@ end | NONE => []) -fun is_fact type_sys conjecture_shape = - not o null o resolve_fact type_sys 0 conjecture_shape +fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape fun resolve_conjecture _ (_, SOME s) = (case try (unprefix conjecture_prefix) s of @@ -215,29 +211,29 @@ else isa_ext -fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) = - union (op =) (resolve_fact type_sys facts_offset fact_names name) - | add_fact ctxt _ _ _ (Inference (_, _, deps)) = +fun add_fact _ facts_offset fact_names (Inference (name, _, [])) = + union (op =) (resolve_fact facts_offset fact_names name) + | add_fact ctxt _ _ (Inference (_, _, deps)) = if AList.defined (op =) deps leo2_ext then insert (op =) (ext_name ctxt, General (* or Chained... *)) else I - | add_fact _ _ _ _ _ = I + | add_fact _ _ _ _ = I -fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof = +fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof = if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names - else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof [] + else fold (add_fact ctxt facts_offset fact_names) atp_proof [] fun is_conjecture_used_in_proof conjecture_shape = exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) -fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset +fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset fact_names atp_proof = let val used_facts = - used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof + used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof in if forall (is_locality_global o snd) used_facts andalso not (is_conjecture_used_in_proof conjecture_shape atp_proof) then @@ -653,12 +649,11 @@ (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) -fun add_line _ _ _ (line as Definition _) lines = line :: lines - | add_line type_sys conjecture_shape fact_names (Inference (name, t, [])) - lines = +fun add_line _ _ (line as Definition _) lines = line :: lines + | add_line conjecture_shape fact_names (Inference (name, t, [])) lines = (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) - if is_fact type_sys fact_names name then + if is_fact fact_names name then (* Facts are not proof lines. *) if is_only_type_information t then map (replace_dependencies_in_line (name, [])) lines @@ -672,7 +667,7 @@ Inference (name, s_not t, []) :: lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ _ _ (Inference (name, t, deps)) lines = + | add_line _ _ (Inference (name, t, deps)) lines = (* Type information will be deleted later; skip repetition test. *) if is_only_type_information t then Inference (name, t, deps) :: lines @@ -700,13 +695,12 @@ fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false -fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) = +fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names - frees (Inference (name, t, deps)) (j, lines) = + | add_desired_line isar_shrink_factor conjecture_shape fact_names frees + (Inference (name, t, deps)) (j, lines) = (j + 1, - if is_fact type_sys fact_names name orelse - is_conjecture conjecture_shape name orelse + if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse (* the last line must be kept *) j = 0 orelse (not (is_only_type_information t) andalso @@ -741,24 +735,22 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) -fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names - name = - if is_fact type_sys fact_names name then - apsnd (union (op =) - (map fst (resolve_fact type_sys facts_offset 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 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 type_sys conjecture_shape facts_offset - 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 type_sys conjecture_shape - facts_offset fact_names) + ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset + fact_names) deps ([], []))) fun repair_name "$true" = "c_True" @@ -772,9 +764,8 @@ else s -fun isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor - conjecture_shape facts_offset fact_names sym_tab params frees - atp_proof = +fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape + facts_offset fact_names sym_tab params frees atp_proof = let val lines = atp_proof @@ -782,15 +773,15 @@ |> nasty_atp_proof pool |> map_term_names_in_atp_proof repair_name |> decode_lines ctxt sym_tab - |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names) + |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) - |-> fold_rev (add_desired_line type_sys isar_shrink_factor - conjecture_shape fact_names frees) + |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape + fact_names frees) |> snd in (if null params then [] else [Fix params]) @ - map2 (step_for_line type_sys conjecture_shape facts_offset fact_names) + map2 (step_for_line conjecture_shape facts_offset fact_names) (length lines downto 1) lines end @@ -1084,8 +1075,8 @@ in do_proof end fun isar_proof_text ctxt isar_proof_requested - (debug, full_types, isar_shrink_factor, type_sys, pool, - conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal) + (debug, full_types, isar_shrink_factor, pool, conjecture_shape, + facts_offset, fact_names, sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let val isar_shrink_factor = @@ -1095,7 +1086,7 @@ val one_line_proof = one_line_proof_text one_line_params fun isar_proof_for () = case atp_proof - |> isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor + |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape facts_offset fact_names sym_tab params frees |> redirect_proof hyp_ts concl_t |> kill_duplicate_assumptions_in_proof diff -r c4ea897a5326 -r 6901ebafbb8d src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 00:16:28 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 00:16:28 2011 +0200 @@ -130,7 +130,8 @@ val type_constrs_of_terms : theory -> term list -> string list val prepare_atp_problem : Proof.context -> format -> formula_kind -> formula_kind -> type_sys - -> bool -> bool -> term list -> term -> ((string * locality) * term) list + -> bool -> bool -> bool -> term list -> term + -> ((string * locality) * term) list -> string problem * string Symtab.table * int * int * (string * locality) list vector * int list * int Symtab.table val atp_problem_weights : string problem -> (string * real) list @@ -1547,12 +1548,8 @@ the remote provers might care. *) fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys (j, formula as {name, locality, kind, ...}) = - Formula (prefix ^ - (if freshen andalso - polymorphism_of_type_sys type_sys <> Polymorphic then - string_of_int j ^ "_" - else - "") ^ encode name, + Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ + encode name, kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE, case locality of Intro => intro_info @@ -1838,7 +1835,7 @@ val explicit_apply = NONE (* for experimental purposes *) fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - readable_names preproc hyp_ts concl_t facts = + freshen_facts readable_names preproc hyp_ts concl_t facts = let val (format, type_sys) = choose_format [format] type_sys val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = @@ -1877,8 +1874,8 @@ val problem = [(explicit_declsN, sym_decl_lines), (factsN, - map (formula_line_for_fact ctxt format fact_prefix ascii_of true - nonmono_Ts type_sys) + map (formula_line_for_fact ctxt format fact_prefix ascii_of + freshen_facts nonmono_Ts type_sys) (0 upto length facts - 1 ~~ facts)), (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), (aritiesN, map formula_line_for_arity_clause arity_clauses), diff -r c4ea897a5326 -r 6901ebafbb8d src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Thu Jun 09 00:16:28 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Jun 09 00:16:28 2011 +0200 @@ -198,8 +198,8 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) *) val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false [] - @{prop False} props + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false + [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) diff -r c4ea897a5326 -r 6901ebafbb8d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 09 00:16:28 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jun 09 00:16:28 2011 +0200 @@ -649,8 +649,8 @@ val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_sys (Config.get ctxt atp_readable_names) true hyp_ts - concl_t facts + type_sys true (Config.get ctxt atp_readable_names) true + hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^ @@ -685,7 +685,7 @@ val (conjecture_shape, facts_offset, fact_names, typed_helpers) = if is_none outcome then - repair_conjecture_shape_and_fact_names type_sys output + repair_conjecture_shape_and_fact_names output conjecture_shape facts_offset fact_names typed_helpers else (* don't bother repairing *) @@ -693,7 +693,7 @@ val outcome = case outcome of NONE => - used_facts_in_unsound_atp_proof ctxt type_sys + used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset fact_names atp_proof |> Option.map (fn facts => UnsoundProof (is_type_sys_virtually_sound type_sys, @@ -704,11 +704,11 @@ in ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers, sym_tab), - (output, msecs, type_sys, atp_proof, outcome)) + (output, msecs, atp_proof, outcome)) end val timer = Timer.startRealTimer () fun maybe_run_slice blacklist slice - (result as (_, (_, msecs0, _, _, SOME _))) = + (result as (_, (_, msecs0, _, SOME _))) = let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in @@ -716,18 +716,17 @@ result else (run_slice blacklist slice time_left - |> (fn (stuff, (output, msecs, type_sys, atp_proof, - outcome)) => - (stuff, (output, int_opt_add msecs0 msecs, type_sys, + |> (fn (stuff, (output, msecs, atp_proof, outcome)) => + (stuff, (output, int_opt_add msecs0 msecs, atp_proof, outcome)))) end | maybe_run_slice _ _ result = result fun maybe_blacklist_facts_and_retry iter blacklist (result as ((_, _, facts_offset, fact_names, _, _), - (_, _, type_sys, atp_proof, + (_, _, atp_proof, SOME (UnsoundProof (false, _))))) = - (case used_facts_in_atp_proof ctxt type_sys facts_offset - fact_names atp_proof of + (case used_facts_in_atp_proof ctxt facts_offset fact_names + atp_proof of [] => result | new_baddies => if slicing andalso iter < atp_blacklist_max_iters - 1 then @@ -741,8 +740,7 @@ | maybe_blacklist_facts_and_retry _ _ result = result in ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty), - ("", SOME 0, hd fallback_best_type_systems, [], - SOME InternalError)) + ("", SOME 0, [], SOME InternalError)) |> fold (maybe_run_slice []) actual_slices (* The ATP found an unsound proof? Automatically try again without the offending facts! *) @@ -755,14 +753,14 @@ the proof file too. *) fun cleanup prob_file = if dest_dir = "" then try File.rm prob_file else NONE - fun export prob_file (_, (output, _, _, _, _)) = + fun export prob_file (_, (output, _, _, _)) = if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers, sym_tab), - (output, msecs, type_sys, atp_proof, outcome)) = + (output, msecs, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = if mode = Normal andalso @@ -775,8 +773,7 @@ NONE => let val used_facts = - used_facts_in_atp_proof ctxt type_sys facts_offset fact_names - atp_proof + used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof in (used_facts, fn () => @@ -792,9 +789,9 @@ let val full_types = uses_typed_helpers typed_helpers atp_proof val isar_params = - (debug, full_types, isar_shrink_factor, type_sys, pool, - conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, - goal) + (debug, full_types, isar_shrink_factor, pool, + conjecture_shape, facts_offset, fact_names, sym_tab, + atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command minimize_command name preplay,