always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 21 10:31:48 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 21 10:42:29 2011 +0100
@@ -24,14 +24,14 @@
val subst = []
val case_names = case_const_names ctxt stds
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
-val def_table = const_def_table ctxt subst defs
+val def_tables = const_def_tables ctxt subst defs
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
val user_nondefs =
user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
-val intro_table = inductive_intro_table ctxt subst def_table
+val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {thy, ...} : hol_context =
@@ -40,7 +40,7 @@
whacks = [], binary_ints = SOME false, destroy_constrs = true,
specialize = false, star_linear_preds = false,
tac_timeout = NONE, evals = [], case_names = case_names,
- def_table = def_table, nondef_table = nondef_table,
+ def_tables = def_tables, nondef_table = nondef_table,
user_nondefs = user_nondefs, simp_table = simp_table,
psimp_table = psimp_table, choice_spec_table = choice_spec_table,
intro_table = intro_table, ground_thm_table = ground_thm_table,
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 10:31:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 10:42:29 2011 +0100
@@ -265,14 +265,14 @@
val max_bisim_depth = fold Integer.max bisim_depths ~1
val case_names = case_const_names ctxt stds
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst
- val def_table = const_def_table ctxt subst defs
+ val def_tables = const_def_tables ctxt subst defs
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
val user_nondefs =
user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
- val intro_table = inductive_intro_table ctxt subst def_table
+ val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {wf_cache, ...} =
@@ -281,7 +281,7 @@
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_table = def_table,
+ evals = evals, case_names = case_names, def_tables = def_tables,
nondef_table = nondef_table, user_nondefs = user_nondefs,
simp_table = simp_table, psimp_table = psimp_table,
choice_spec_table = choice_spec_table, intro_table = intro_table,
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 10:31:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 10:42:29 2011 +0100
@@ -30,7 +30,7 @@
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
- def_table: const_table,
+ def_tables: const_table * const_table,
nondef_table: const_table,
user_nondefs: term list,
simp_table: const_table Unsynchronized.ref,
@@ -187,15 +187,17 @@
val case_const_names :
Proof.context -> (typ option * bool) list -> (string * int) list
val unfold_defs_in_term : hol_context -> term -> term
- val const_def_table :
- Proof.context -> (term * term) list -> term list -> const_table
+ val const_def_tables :
+ Proof.context -> (term * term) list -> term list
+ -> const_table * const_table
val const_nondef_table : term list -> const_table
val const_simp_table : Proof.context -> (term * term) list -> const_table
val const_psimp_table : Proof.context -> (term * term) list -> const_table
val const_choice_spec_table :
Proof.context -> (term * term) list -> const_table
val inductive_intro_table :
- Proof.context -> (term * term) list -> const_table -> const_table
+ Proof.context -> (term * term) list -> const_table * const_table
+ -> const_table
val ground_theorem_table : theory -> term list Inttab.table
val ersatz_table : Proof.context -> (string * string) list
val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
@@ -203,10 +205,10 @@
val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
val optimized_quot_type_axioms :
Proof.context -> (typ option * bool) list -> string * typ list -> term list
- val def_of_const : theory -> const_table -> styp -> term option
+ val def_of_const : theory -> const_table * const_table -> styp -> term option
val fixpoint_kind_of_rhs : term -> fixpoint_kind
val fixpoint_kind_of_const :
- theory -> const_table -> string * typ -> fixpoint_kind
+ theory -> const_table * const_table -> string * typ -> fixpoint_kind
val is_real_inductive_pred : hol_context -> styp -> bool
val is_constr_pattern_lhs : Proof.context -> term -> bool
val is_constr_pattern_formula : Proof.context -> term -> bool
@@ -256,7 +258,7 @@
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
- def_table: const_table,
+ def_tables: const_table * const_table,
nondef_table: const_table,
user_nondefs: term list,
simp_table: const_table Unsynchronized.ref,
@@ -1376,14 +1378,19 @@
val args = strip_comb lhs |> snd
in fold_rev aux args (SOME rhs) end
-fun def_of_const thy table (x as (s, _)) =
- if is_built_in_const thy [(NONE, false)] x orelse
- original_name s <> s then
+fun get_def_of_const thy table (x as (s, _)) =
+ x |> def_props_for_const thy [(NONE, false)] table |> List.last
+ |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
+ handle List.Empty => NONE
+
+fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
+ if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
NONE
- else
- x |> def_props_for_const thy [(NONE, false)] table |> List.last
- |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
- handle List.Empty => NONE
+ else case get_def_of_const thy unfold_table x of
+ SOME def => SOME (true, def)
+ | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false)
+
+val def_of_const = Option.map snd ooo def_of_const_ext
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
| fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
@@ -1434,9 +1441,9 @@
else fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-fun is_real_inductive_pred ({thy, stds, def_table, intro_table, ...}
+fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
: hol_context) x =
- fixpoint_kind_of_const thy def_table x <> NoFp andalso
+ fixpoint_kind_of_const thy def_tables x <> NoFp andalso
not (null (def_props_for_const thy stds intro_table x))
fun is_inductive_pred hol_ctxt (x as (s, _)) =
is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
@@ -1502,11 +1509,11 @@
#> Object_Logic.atomize_term thy
#> Choice_Specification.close_form
#> HOLogic.mk_Trueprop
-fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
+fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
: hol_context) x =
case nondef_props_for_const thy true choice_spec_table x of
[] => false
- | ts => case def_of_const thy def_table x of
+ | ts => case def_of_const thy def_tables x of
SOME (Const (@{const_name Eps}, _) $ _) => true
| SOME _ => false
| NONE =>
@@ -1614,7 +1621,7 @@
val def_inline_threshold_for_non_booleans = 20
fun unfold_defs_in_term
- (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_table,
+ (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
ground_thm_table, ersatz_table, ...}) =
let
fun do_term depth Ts t =
@@ -1781,8 +1788,8 @@
else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
is_choice_spec_fun hol_ctxt x then
(Const x, ts)
- else case def_of_const thy def_table x of
- SOME def =>
+ else case def_of_const_ext thy def_tables x of
+ SOME (unfold, def) =>
if depth > unfold_max_depth then
raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
"too many nested definitions (" ^
@@ -1790,7 +1797,8 @@
quote s)
else if s = @{const_name wfrec'} then
(do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
- else if size_of_term def > def_inline_threshold () then
+ else if not unfold andalso
+ size_of_term def > def_inline_threshold () then
(Const x, ts)
else
(do_term (depth + 1) Ts def, ts)
@@ -1841,10 +1849,10 @@
ctxt |> get |> map (pair_for_prop o subst_atomic subst)
|> AList.group (op =) |> Symtab.make
-fun const_def_table ctxt subst ts =
- def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
- |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
- (map pair_for_prop ts)
+fun const_def_tables ctxt subst ts =
+ (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst,
+ fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
+ (map pair_for_prop ts) Symtab.empty)
fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
fun const_nondef_table ts =
@@ -1861,10 +1869,10 @@
map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
|> const_nondef_table
-fun inductive_intro_table ctxt subst def_table =
+fun inductive_intro_table ctxt subst def_tables =
let val thy = ProofContext.theory_of ctxt in
def_table_for
- (maps (map (unfold_mutually_inductive_preds thy def_table o prop_of)
+ (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
o snd o snd)
o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
cat = Spec_Rules.Co_Inductive)
@@ -2086,7 +2094,7 @@
(* The type constraint below is a workaround for a Poly/ML crash. *)
fun is_well_founded_inductive_pred
- (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
+ (hol_ctxt as {thy, wfs, def_tables, wf_cache, ...} : hol_context)
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
@@ -2095,7 +2103,7 @@
SOME (_, wf) => wf
| NONE =>
let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
in
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
@@ -2214,13 +2222,13 @@
| is_good_starred_linear_pred_type _ = false
fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
- def_table, simp_table, ...})
+ def_tables, simp_table, ...})
gfp (x as (s, T)) =
let
val iter_T = iterator_type_for_const gfp x
val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
val unrolled_const = Const x' $ zero_const iter_T
- val def = the (def_of_const thy def_table x)
+ val def = the (def_of_const thy def_tables x)
in
if is_equational_fun_but_no_plain_def hol_ctxt x' then
unrolled_const (* already done *)
@@ -2251,9 +2259,9 @@
in unrolled_const end
end
-fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
+fun raw_inductive_pred_axiom ({thy, def_tables, ...} : hol_context) x =
let
- val def = the (def_of_const thy def_table x)
+ val def = the (def_of_const thy def_tables x)
val (outer, fp_app) = strip_abs def
val outer_bounds = map Bound (length outer - 1 downto 0)
val rhs =
@@ -2277,13 +2285,13 @@
else
raw_inductive_pred_axiom hol_ctxt x
-fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_table, simp_table,
+fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
psimp_table, ...}) x =
case def_props_for_const thy stds (!simp_table) x of
[] => (case def_props_for_const thy stds psimp_table x of
[] => (if is_inductive_pred hol_ctxt x then
[inductive_pred_axiom hol_ctxt x]
- else case def_of_const thy def_table x of
+ else case def_of_const thy def_tables x of
SOME def =>
@{const Trueprop} $ HOLogic.mk_eq (Const x, def)
|> equationalize_term ctxt "" |> the |> single
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 21 10:31:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 21 10:42:29 2011 +0100
@@ -662,9 +662,9 @@
| dest_n_tuple_type _ T =
raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
-fun const_format thy def_table (x as (s, T)) =
+fun const_format thy def_tables (x as (s, T)) =
if String.isPrefix unrolled_prefix s then
- const_format thy def_table (original_name s, range_type T)
+ const_format thy def_tables (original_name s, range_type T)
else if String.isPrefix skolem_prefix s then
let
val k = unprefix skolem_prefix s
@@ -673,7 +673,7 @@
in [k, num_binder_types T - k] end
else if original_name s <> s then
[num_binder_types T]
- else case def_of_const thy def_table x of
+ else case def_of_const thy def_tables x of
SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
let val k = length (strip_abs_vars t') in
[k, num_binder_types T - k]
@@ -690,7 +690,7 @@
[Int.min (k1, k2)]
end
-fun lookup_format thy def_table formats t =
+fun lookup_format thy def_tables formats t =
case AList.lookup (fn (SOME x, SOME y) =>
(term_match thy) (x, y) | _ => false)
formats (SOME t) of
@@ -698,7 +698,7 @@
| NONE => let val format = the (AList.lookup (op =) formats NONE) in
case t of
Const x => intersect_formats format
- (const_format thy def_table x)
+ (const_format thy def_tables x)
| _ => format
end
@@ -719,16 +719,16 @@
|> map (HOLogic.mk_tupleT o rev)
in List.foldl (op -->) body_T batched end
end
-fun format_term_type thy def_table formats t =
+fun format_term_type thy def_tables formats t =
format_type (the (AList.lookup (op =) formats NONE))
- (lookup_format thy def_table formats t) (fastype_of t)
+ (lookup_format thy def_tables formats t) (fastype_of t)
fun repair_special_format js m format =
m - 1 downto 0 |> chunk_list_unevenly (rev format)
|> map (rev o filter_out (member (op =) js))
|> filter_out null |> map length |> rev
-fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
+fun user_friendly_const ({thy, evals, def_tables, skolems, special_funs, ...}
: hol_context) (base_name, step_name) formats =
let
val default_format = the (AList.lookup (op =) formats NONE)
@@ -762,7 +762,7 @@
SOME format =>
repair_special_format js (num_binder_types T') format
| NONE =>
- const_format thy def_table x'
+ const_format thy def_tables x'
|> repair_special_format js (num_binder_types T')
|> intersect_formats default_format
in
@@ -789,7 +789,7 @@
let val t = Const (original_name s, range_type T) in
(lambda (Free (iter_var_prefix, nat_T)) t,
format_type default_format
- (lookup_format thy def_table formats t) T)
+ (lookup_format thy def_tables formats t) T)
end
else if String.isPrefix base_prefix s then
(Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
@@ -799,7 +799,7 @@
format_type default_format default_format T)
else if String.isPrefix quot_normal_prefix s then
let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
- (t, format_term_type thy def_table formats t)
+ (t, format_term_type thy def_tables formats t)
end
else if String.isPrefix skolem_prefix s then
let
@@ -810,15 +810,15 @@
in
(fold lambda frees (Const (s', Ts' ---> T)),
format_type default_format
- (lookup_format thy def_table formats (Const x)) T)
+ (lookup_format thy def_tables formats (Const x)) T)
end
else if String.isPrefix eval_prefix s then
let
val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
- in (t, format_term_type thy def_table formats t) end
+ in (t, format_term_type thy def_tables formats t) end
else
let val t = Const (original_name s, T) in
- (t, format_term_type thy def_table formats t)
+ (t, format_term_type thy def_tables formats t)
end)
|>> map_types uniterize_unarize_unbox_etc_type
|>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
@@ -863,7 +863,7 @@
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
star_linear_preds, tac_timeout, evals, case_names,
- def_table, nondef_table, user_nondefs, simp_table,
+ def_tables, nondef_table, user_nondefs, simp_table,
psimp_table, choice_spec_table, intro_table,
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache},
@@ -880,7 +880,7 @@
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_table = def_table,
+ evals = evals, case_names = case_names, def_tables = def_tables,
nondef_table = nondef_table, user_nondefs = user_nondefs,
simp_table = simp_table, psimp_table = psimp_table,
choice_spec_table = choice_spec_table, intro_table = intro_table,
@@ -912,7 +912,7 @@
case name of
FreeName (s, T, _) =>
let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
- ("=", (t, format_term_type thy def_table formats t), T)
+ ("=", (t, format_term_type thy def_tables formats t), T)
end
| ConstName (s, T, _) =>
(assign_operator_for_const (s, T),
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 10:31:48 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 10:42:29 2011 +0100
@@ -540,7 +540,7 @@
fun skolem_prefix_for k j =
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
-fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
+fun skolemize_term_and_more (hol_ctxt as {thy, def_tables, skolems, ...})
skolem_depth =
let
val incrs = map (Integer.add 1)
@@ -615,7 +615,7 @@
not (is_real_equational_fun hol_ctxt x) andalso
not (is_well_founded_inductive_pred hol_ctxt x) then
let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
val (pref, connective) =
if gfp then (lbfp_prefix, @{const HOL.disj})
else (ubfp_prefix, @{const HOL.conj})
@@ -729,7 +729,7 @@
forall (op aconv) (ts1 ~~ ts2)
fun specialize_consts_in_term
- (hol_ctxt as {ctxt, thy, stds, specialize, def_table, simp_table,
+ (hol_ctxt as {ctxt, thy, stds, specialize, def_tables, simp_table,
special_funs, ...}) def depth t =
if not specialize orelse depth > special_max_depth then
t
@@ -742,7 +742,7 @@
not (String.isPrefix special_prefix s) andalso
not (is_built_in_const thy stds x) andalso
(is_equational_fun_but_no_plain_def hol_ctxt x orelse
- (is_some (def_of_const thy def_table x) andalso
+ (is_some (def_of_const thy def_tables x) andalso
not (is_of_class_const thy x) andalso
not (is_constr ctxt stds x) andalso
not (is_choice_spec_fun hol_ctxt x))) then
@@ -879,7 +879,8 @@
| NONE => false
fun all_table_entries table = Symtab.fold (append o snd) table []
-fun extra_table table s = Symtab.make [(s, all_table_entries table)]
+fun extra_table tables s =
+ Symtab.make [(s, pairself all_table_entries tables |> op @)]
fun eval_axiom_for_term j t =
Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
@@ -891,7 +892,7 @@
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
- evals, def_table, nondef_table, choice_spec_table,
+ evals, def_tables, nondef_table, choice_spec_table,
user_nondefs, ...}) assm_ts neg_t =
let
val (def_assm_ts, nondef_assm_ts) =
@@ -962,7 +963,7 @@
range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
- (extra_table def_table s) x)
+ (extra_table def_tables s) x)
else if is_rep_fun ctxt x then
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
@@ -970,14 +971,14 @@
range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
- (extra_table def_table s) x)
+ (extra_table def_tables s) x)
|> add_axioms_for_term depth
(Const (mate_of_rep_fun ctxt x))
|> fold (add_def_axiom depth)
(inverse_axioms_for_rep_fun ctxt x)
else if s = @{const_name TYPE} then
accum
- else case def_of_const thy def_table x of
+ else case def_of_const thy def_tables x of
SOME _ =>
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
accum