# HG changeset patch # User blanchet # Date 1281010218 -7200 # Node ID 379fb08da97be3d89b3ff8d9950f4875185be36c # Parent 927f919914ea34e44a270851bc71386148e71b0a prevent the expansion of too large definitions -- use equations for these instead diff -r 927f919914ea -r 379fb08da97b src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 12:58:57 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 14:10:18 2010 +0200 @@ -141,7 +141,6 @@ val sel_no_from_name : string -> int val close_form : term -> term val eta_expand : typ list -> term -> int -> term - val extensionalize : term -> term val distinctness_formula : typ -> term list -> term val register_frac_type : string -> (string * string) list -> theory -> theory val unregister_frac_type : string -> theory -> theory @@ -199,13 +198,14 @@ val fixpoint_kind_of_const : theory -> const_table -> string * typ -> fixpoint_kind val is_inductive_pred : hol_context -> styp -> bool - val is_equational_fun : hol_context -> styp -> bool val is_constr_pattern_lhs : Proof.context -> term -> bool val is_constr_pattern_formula : Proof.context -> term -> bool val nondef_props_for_const : theory -> bool -> const_table -> styp -> term list val is_choice_spec_fun : hol_context -> styp -> bool val is_choice_spec_axiom : theory -> const_table -> term -> bool + val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool + val is_equational_fun : hol_context -> styp -> bool val codatatype_bisim_axioms : hol_context -> typ -> term list val is_well_founded_inductive_pred : hol_context -> styp -> bool val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term @@ -879,15 +879,6 @@ (List.take (binder_types (fastype_of1 (Ts, t)), n)) (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) -fun extensionalize t = - case t of - (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1 - | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) => - let val v = Var ((s, maxidx_of_term t + 1), T) in - extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2))) - end - | _ => t - fun distinctness_formula T = all_distinct_unordered_pairs_of #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) @@ -1418,9 +1409,6 @@ [!simp_table, psimp_table] fun is_inductive_pred hol_ctxt = is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt) -fun is_equational_fun hol_ctxt = - (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf - (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) fun lhs_of_equation t = case t of @@ -1502,6 +1490,14 @@ exists (curry (op aconv) t o axiom_for_choice_spec thy) ts) choice_spec_table +fun is_equational_fun_but_no_plain_def hol_ctxt = + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf + (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) +fun is_equational_fun (hol_ctxt as {ctxt, thy, def_table, ...}) (x as (s, _)) = + is_equational_fun_but_no_plain_def hol_ctxt x orelse + (not (is_choice_spec_fun hol_ctxt x) andalso + is_some (def_of_const thy def_table x)) + (** Constant unfolding **) fun constr_case_body ctxt stds (func_t, (x as (_, T))) = @@ -1581,6 +1577,9 @@ (* Prevents divergence in case of cyclic or infinite definition dependencies. *) val unfold_max_depth = 255 +(* Inline definitions or define as an equational constant? *) +val def_inline_threshold = 20 + fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names, def_table, ground_thm_table, ersatz_table, ...}) = @@ -1704,7 +1703,7 @@ else (Const x, ts) end - else if is_equational_fun hol_ctxt x orelse + 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 @@ -1716,6 +1715,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 + (Const x, ts) else (do_term (depth + 1) Ts def, ts) | NONE => (Const x, ts) @@ -1727,7 +1728,7 @@ (** Axiom extraction/generation **) -fun equationalize ctxt tag t = +fun equationalize_term ctxt tag t = let val (prems, concl) = Logic.strip_horn t in Logic.list_implies (prems, case concl of @@ -1764,10 +1765,10 @@ fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make fun const_simp_table ctxt = - def_table_for (map_filter (equationalize ctxt "nitpick_simp" o prop_of) + def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of) o Nitpick_Simps.get) ctxt fun const_psimp_table ctxt = - def_table_for (map_filter (equationalize ctxt "nitpick_psimp" o prop_of) + def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of) o Nitpick_Psimps.get) ctxt fun const_choice_spec_table ctxt subst = @@ -2132,7 +2133,7 @@ val unrolled_const = Const x' $ zero_const iter_T val def = the (def_of_const thy def_table x) in - if is_equational_fun hol_ctxt x' then + if is_equational_fun_but_no_plain_def hol_ctxt x' then unrolled_const (* already done *) else if not gfp andalso star_linear_preds andalso is_linear_inductive_pred_def def andalso @@ -2187,16 +2188,21 @@ else raw_inductive_pred_axiom hol_ctxt x -fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table, - psimp_table, ...}) x = +fun equational_fun_axioms (hol_ctxt as {ctxt, thy, stds, fast_descrs, def_table, + simp_table, psimp_table, ...}) x = case def_props_for_const thy stds fast_descrs (!simp_table) x of [] => (case def_props_for_const thy stds fast_descrs psimp_table x of - [] => [inductive_pred_axiom hol_ctxt x] + [] => (if is_inductive_pred hol_ctxt x then + [inductive_pred_axiom hol_ctxt x] + else case def_of_const thy def_table x of + SOME def => + @{const Trueprop} $ HOLogic.mk_eq (Const x, def) + |> equationalize_term ctxt "" |> the |> single + | NONE => []) | psimps => psimps) | simps => simps -val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms fun is_equational_fun_surely_complete hol_ctxt x = - case raw_equational_fun_axioms hol_ctxt x of + case equational_fun_axioms hol_ctxt x of [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] => strip_comb t1 |> snd |> forall is_Var | _ => false diff -r 927f919914ea -r 379fb08da97b src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 12:58:57 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 14:10:18 2010 +0200 @@ -946,7 +946,7 @@ else if is_descr (original_name s) then fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x) accum - else if is_equational_fun hol_ctxt x then + else if is_equational_fun_but_no_plain_def hol_ctxt x then fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) accum else if is_choice_spec_fun hol_ctxt x then @@ -980,7 +980,11 @@ (inverse_axioms_for_rep_fun ctxt x) else if s = @{const_name TYPE} then accum - else + else case def_of_const thy def_table x of + SOME def => + fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) + accum + | NONE => accum |> user_axioms <> SOME false ? fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x)