# HG changeset patch # User wenzelm # Date 1444061038 -7200 # Node ID fa7a46489285281a6a7c96d76e859ba9e810ac3f # Parent 1cfc476198c937820239c0c40e7b826168ae7e46# Parent 0a4c364df4312ceb07951b9736f2e014ace45472 merged diff -r 0a4c364df431 -r fa7a46489285 NEWS --- a/NEWS Mon Oct 05 18:03:52 2015 +0200 +++ b/NEWS Mon Oct 05 18:03:58 2015 +0200 @@ -253,6 +253,8 @@ - Eliminated obsolete "blocking" option and related subcommands. * Nitpick: + - Fixed soundness bug in translation of "finite" predicate. + - Fixed soundness bug in "destroy_constrs" optimization. - Removed "check_potential" and "check_genuine" options. - Eliminated obsolete "blocking" option. diff -r 0a4c364df431 -r fa7a46489285 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Oct 05 18:03:58 2015 +0200 @@ -18,8 +18,17 @@ ML {* val do_it = false (* switch to "true" to generate the files *) val ctxt = @{context} -val thy = @{theory List} -val infer_policy = Unchecked_Inferences +val thy = @{theory Complex_Main} +val infer_policy = (* Unchecked_Inferences *) No_Inferences +*} + +ML {* +if do_it then + "/tmp/isa_filter" + |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice)) + infer_policy "poly_native_higher" +else + () *} ML {* diff -r 0a4c364df431 -r fa7a46489285 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Oct 05 18:03:58 2015 +0200 @@ -12,12 +12,10 @@ datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences - val generate_atp_inference_file_for_theory : - Proof.context -> theory -> atp_format -> inference_policy -> string - -> string -> unit - val generate_casc_lbt_isa_files_for_theory : - Proof.context -> theory -> atp_format -> inference_policy -> string - -> string -> unit + val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format -> + inference_policy -> string -> string -> unit + val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format -> + inference_policy -> string -> string -> unit end; structure ATP_Theory_Export : ATP_THEORY_EXPORT = @@ -28,6 +26,10 @@ open ATP_Problem_Generate open ATP_Systems +val max_dependencies = 100 +val max_facts = 512 +val atp_timeout = seconds 0.5 + datatype inference_policy = No_Inferences | Unchecked_Inferences | Checked_Inferences @@ -44,8 +46,6 @@ | atp_of_format CNF_UEQ = waldmeisterN | atp_of_format CNF = eN -val atp_timeout = seconds 0.5 - fun run_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt @@ -53,8 +53,9 @@ val atp = atp_of_format format val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp - val _ = problem |> lines_of_atp_problem format ord (K []) - |> File.write_list prob_file + val _ = problem + |> lines_of_atp_problem format ord (K []) + |> File.write_list prob_file val exec = exec false val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = @@ -111,14 +112,14 @@ fun add_inferences_to_problem ctxt format check_infs prelude infers problem = let - fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = - Symtab.default (ident, axiom) + fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom) | add_if_axiom _ = I + val add_axioms_of_problem = fold (fold add_if_axiom o snd) val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem in - map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs - prelude axioms infers))) problem + map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers))) + problem end fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident @@ -139,8 +140,7 @@ [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, @{typ unit}] -fun ground_type_of_tvar _ [] tvar = - raise TYPE ("ground_type_of_tvar", [TVar tvar], []) +fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], []) | ground_type_of_tvar thy (T :: Ts) tvar = if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T else ground_type_of_tvar thy Ts tvar @@ -152,9 +152,7 @@ end fun heading_sort_key heading = - if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading - -val max_dependencies = 100 + if String.isPrefix factsN heading then "_" ^ heading else heading fun problem_of_theory ctxt thy format infer_policy type_enc = let @@ -163,6 +161,7 @@ type_enc |> type_enc_of_string Non_Strict |> adjust_type_enc format val mono = not (is_type_enc_polymorphic type_enc) + val facts = Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false Keyword.empty_keywords [] [] css_table @@ -204,12 +203,13 @@ |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names)) val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab) in - problem - |> (case format of + (facts, + problem + |> (case format of DFG _ => I - | _ => add_inferences_to_problem ctxt format - (infer_policy = Checked_Inferences) prelude infers) - |> order_problem_facts name_ord + | _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude + infers) + |> order_problem_facts name_ord) end fun lines_of_problem ctxt format = @@ -224,7 +224,7 @@ fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name = let - val problem = problem_of_theory ctxt thy format infer_policy type_enc + val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc val ss = lines_of_problem ctxt format problem in write_lines (Path.explode file_name) ss end @@ -248,11 +248,13 @@ | theory_name_of_fact _ = "" val problem_suffix = ".p" +val suggestion_suffix = ".sugg" val include_suffix = ".ax" val file_order_name = "FilesInProcessingOrder" val problem_order_name = "ProblemsInProcessingOrder" val problem_name = "problems" +val suggestion_name = "suggestions" val include_name = "incl" val prelude_base_name = "prelude" val prelude_name = prelude_base_name ^ include_suffix @@ -280,8 +282,11 @@ base_name ^ "__" ^ string_of_int n ^ "_" ^ perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix -fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc - dir_name = +fun suggestion_name_of base_name n alt = + base_name ^ "__" ^ string_of_int n ^ "_" ^ + perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix + +fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name = let val dir = Path.explode dir_name val _ = Isabelle_System.mkdir dir @@ -291,55 +296,79 @@ val _ = File.write problem_order_path "" val problem_dir = ap dir problem_name val _ = Isabelle_System.mkdir problem_dir + val suggestion_dir = ap dir suggestion_name + val _ = Isabelle_System.mkdir suggestion_dir val include_dir = ap problem_dir include_name val _ = Isabelle_System.mkdir include_dir - val (prelude, groups) = + + val (facts, (prelude, groups)) = problem_of_theory ctxt thy format infer_policy type_enc - |> split_last - ||> (snd + ||> split_last + ||> apsnd (snd #> chop_maximal_groups (op = o apply2 theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) + + val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts) + fun write_prelude () = let val ss = lines_of_problem ctxt format prelude in File.append file_order_path (prelude_base_name ^ "\n"); write_lines (ap include_dir prelude_name) ss end - fun write_include_file (base_name, facts) = + + fun write_include_file (base_name, fact_lines) = let val name = base_name ^ include_suffix - val ss = lines_of_problem ctxt format [(factsN, facts)] + val ss = lines_of_problem ctxt format [(factsN, fact_lines)] in File.append file_order_path (base_name ^ "\n"); write_lines (ap include_dir name) ss end - fun write_problem_files _ _ _ [] = () - | write_problem_files _ includes [] groups = - write_problem_files 1 includes includes groups - | write_problem_files n includes _ ((base_name, []) :: groups) = - write_problem_files n (includes @ [include_line base_name]) [] groups - | write_problem_files n includes seen - ((base_name, fact :: facts) :: groups) = - let val fact_s = tptp_string_of_line format fact in - (if should_generate_problem thy base_name fact then + + fun select_facts_for_fact facts fact = + let + val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact)) + val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt + (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts + in + map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo + end + + fun write_problem_files _ _ _ _ [] = () + | write_problem_files _ seen_facts includes [] groups = + write_problem_files 1 seen_facts includes includes groups + | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) = + write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups + | write_problem_files n seen_facts includes seen_ss + ((base_name, fact_line :: fact_lines) :: groups) = + let + val (ident, alt, pname, sname, conj) = + (case fact_line of + Formula ((ident, alt), _, phi, _, _) => + (ident, alt, problem_name_of base_name n (encode_meta alt), + suggestion_name_of base_name n (encode_meta alt), + Formula ((ident, alt), Conjecture, phi, NONE, []))) + + val fact = the (Symtab.lookup fact_tab alt) + val fact_s = tptp_string_of_line format fact_line + in + (if should_generate_problem thy base_name fact_line then let - val (name, conj) = - (case fact of - Formula ((ident, alt), _, phi, _, _) => - (problem_name_of base_name n (encode_meta alt), - Formula ((ident, alt), Conjecture, phi, NONE, []))) val conj_s = tptp_string_of_line format conj in - File.append problem_order_path (name ^ "\n"); - write_lines (ap problem_dir name) (seen @ [conj_s]) + File.append problem_order_path (pname ^ "\n"); + write_lines (ap problem_dir pname) (seen_ss @ [conj_s]); + write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact) end else (); - write_problem_files (n + 1) includes (seen @ [fact_s]) - ((base_name, facts) :: groups)) + write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s]) + ((base_name, fact_lines) :: groups)) end + val _ = write_prelude () val _ = app write_include_file groups - val _ = write_problem_files 1 [include_line prelude_base_name] [] groups + val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups in () end end; diff -r 0a4c364df431 -r fa7a46489285 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 05 18:03:58 2015 +0200 @@ -390,12 +390,12 @@ (@{const_name unknown}, 0), (@{const_name is_unknown}, 1), (@{const_name safe_The}, 1), - (@{const_name Nitpick.Frac}, 0), - (@{const_name Nitpick.norm_frac}, 0), + (@{const_name Frac}, 0), + (@{const_name norm_frac}, 0), (@{const_name Suc}, 0), (@{const_name nat}, 0), - (@{const_name Nitpick.nat_gcd}, 0), - (@{const_name Nitpick.nat_lcm}, 0)] + (@{const_name nat_gcd}, 0), + (@{const_name nat_lcm}, 0)] val built_in_typed_consts = [((@{const_name zero_class.zero}, nat_T), 0), ((@{const_name one_class.one}, nat_T), 0), @@ -583,9 +583,9 @@ fun typedef_info ctxt s = if is_frac_type ctxt (Type (s, [])) then SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, - Abs_name = @{const_name Nitpick.Abs_Frac}, - Rep_name = @{const_name Nitpick.Rep_Frac}, - prop_of_Rep = @{prop "Nitpick.Rep_Frac x \ Collect Nitpick.Frac"} + Abs_name = @{const_name Abs_Frac}, + Rep_name = @{const_name Rep_Frac}, + prop_of_Rep = @{prop "Rep_Frac x \ Collect Frac"} |> Logic.varify_global, Abs_inverse = NONE, Rep_inverse = NONE} else case Typedef.get_info ctxt s of @@ -859,7 +859,7 @@ fun is_stale_constr ctxt (x as (s, T)) = is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso - not (s = @{const_name Nitpick.Abs_Frac} orelse is_registered_coconstr ctxt x) + not (s = @{const_name Abs_Frac} orelse is_registered_coconstr ctxt x) fun is_constr ctxt (x as (_, T)) = is_nonfree_constr ctxt x andalso diff -r 0a4c364df431 -r fa7a46489285 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Oct 05 18:03:58 2015 +0200 @@ -787,8 +787,8 @@ case polar of Neut => if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) - else KK.True - | Pos => formula_for_bool (not opt1) + else KK.True (* sound? *) + | Pos => KK.False | Neg => KK.True end | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1) diff -r 0a4c364df431 -r fa7a46489285 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Oct 05 18:03:58 2015 +0200 @@ -579,7 +579,7 @@ |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) |> dest_n_tuple (length uncur_arg_Ts) val t = - if constr_s = @{const_name Nitpick.Abs_Frac} then + if constr_s = @{const_name Abs_Frac} then case ts of [Const (@{const_name Pair}, _) $ t1 $ t2] => frac_from_term_pair (body_type T) t1 t2 diff -r 0a4c364df431 -r fa7a46489285 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Oct 05 18:03:58 2015 +0200 @@ -569,8 +569,8 @@ Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) else do_apply t0 ts - | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any) - | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any) + | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any) + | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any) | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) => if is_built_in_const x then let val num_T = domain_type T in @@ -586,8 +586,8 @@ | (Const (@{const_name safe_The}, Type (@{type_name fun}, [_, T2])), [t1]) => Op1 (SafeThe, T2, Any, sub t1) - | (Const (@{const_name Nitpick.Frac}, T), []) => Cst (Fracs, T, Any) - | (Const (@{const_name Nitpick.norm_frac}, T), []) => + | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) + | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => Cst (NatToInt, T, Any) diff -r 0a4c364df431 -r fa7a46489285 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Oct 05 18:03:52 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Oct 05 18:03:58 2015 +0200 @@ -46,9 +46,9 @@ | aux def (t as Const (s, _)) = (not def orelse t <> @{const Suc}) andalso not (member (op =) - [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac}, - @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm}, - @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s) + [@{const_name Abs_Frac}, @{const_name Rep_Frac}, + @{const_name nat_gcd}, @{const_name nat_lcm}, + @{const_name Frac}, @{const_name norm_frac}] s) | aux def (Abs (_, _, t')) = aux def t' | aux _ _ = true in aux end @@ -1055,15 +1055,15 @@ fun simplify_constrs_and_sels ctxt t = let - fun is_nth_sel_on t' n (Const (s, _) $ t) = + fun is_nth_sel_on constr_s t' n (Const (s, _) $ t) = (t = t' andalso is_sel_like_and_no_discr s andalso - sel_no_from_name s = n) - | is_nth_sel_on _ _ _ = false - fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _) - $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] = + constr_name_for_sel_like s = constr_s andalso sel_no_from_name s = n) + | is_nth_sel_on _ _ _ _ = false + fun do_term (Const (@{const_name Rep_Frac}, _) + $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] - | do_term (Const (@{const_name Nitpick.Abs_Frac}, _) - $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] = + | do_term (Const (@{const_name Abs_Frac}, _) + $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) | do_term (t as Const (x as (s, T))) (args as _ :: _) = @@ -1072,7 +1072,7 @@ case hd args of Const (_, T') $ t' => if domain_type T' = body_type T andalso - forall (uncurry (is_nth_sel_on t')) + forall (uncurry (is_nth_sel_on s t')) (index_seq 0 (length args) ~~ args) then t' else