--- 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.
--- 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 {*
--- 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;
--- 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 \<in> Collect Nitpick.Frac"}
+ Abs_name = @{const_name Abs_Frac},
+ Rep_name = @{const_name Rep_Frac},
+ prop_of_Rep = @{prop "Rep_Frac x \<in> 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
--- 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)
--- 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
--- 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)
--- 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