# HG changeset patch # User blanchet # Date 1298281349 -3600 # Node ID 01d722707a361678b834c2648fd516b1a1a94771 # Parent 56dcd46ddf7a167fffd2f114b21ba85b12d0cb10 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp" diff -r 56dcd46ddf7a -r 01d722707a36 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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, diff -r 56dcd46ddf7a -r 01d722707a36 src/HOL/Tools/Nitpick/nitpick.ML --- 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, diff -r 56dcd46ddf7a -r 01d722707a36 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 56dcd46ddf7a -r 01d722707a36 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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), diff -r 56dcd46ddf7a -r 01d722707a36 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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