# HG changeset patch # User blanchet # Date 1281015894 -7200 # Node ID 78403fcd0ec5c72de8c7acea5bce77575361c603 # Parent 37a7272cb453f7ac205d7b00822803d8772c4dd9 fiddle with specialization etc. diff -r 37a7272cb453 -r 78403fcd0ec5 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 14:45:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 05 15:44:54 2010 +0200 @@ -1573,8 +1573,10 @@ (* 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 +(* Inline definitions or define as an equational constant? Booleans tend to + benefit more from inlining, due to the polarity analysis. *) +val def_inline_threshold_for_booleans = 50 +val def_inline_threshold_for_non_booleans = 20 fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names, def_table, ground_thm_table, ersatz_table, @@ -1641,6 +1643,11 @@ do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts | NONE => let + fun def_inline_threshold () = + if is_boolean_type (nth_range_type (length ts) T) then + def_inline_threshold_for_booleans + else + def_inline_threshold_for_non_booleans val (const, ts) = if is_built_in_const thy stds fast_descrs x then (Const x, ts) @@ -1711,7 +1718,7 @@ 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 size_of_term def > def_inline_threshold () then (Const x, ts) else (do_term (depth + 1) Ts def, ts) @@ -1724,17 +1731,28 @@ (** Axiom extraction/generation **) +fun extensional_equal j (Type (@{type_name fun}, [dom_T, ran_T])) t1 t2 = + let val var_t = Var (("x", j), dom_T) in + extensional_equal (j + 1) ran_T (betapply (t1, var_t)) + (betapply (t2, var_t)) + end + | extensional_equal _ T t1 t2 = + Const (@{const_name "op ="}, T --> T --> bool_T) $ t1 $ t2 + fun equationalize_term ctxt tag t = - let val (prems, concl) = Logic.strip_horn t in + let + val j = maxidx_of_term t + 1 + val (prems, concl) = Logic.strip_horn t + in Logic.list_implies (prems, case concl of - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _) => - extensionalize_term concl + @{const Trueprop} $ (Const (@{const_name "op ="}, Type (_, [T, _])) + $ t1 $ t2) => + @{const Trueprop} $ extensional_equal j T t1 t2 | @{const Trueprop} $ t' => @{const Trueprop} $ HOLogic.mk_eq (t', @{const True}) | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => - extensionalize_term (Const (@{const_name "op ="}, T --> T --> bool_T) - $ t1 $ t2) + @{const Trueprop} $ extensional_equal j T t1 t2 | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^ quote (Syntax.string_of_term ctxt t) ^ "."); raise SAME ())) diff -r 37a7272cb453 -r 78403fcd0ec5 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 14:45:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 05 15:44:54 2010 +0200 @@ -733,13 +733,13 @@ fun specialize_consts_in_term (hol_ctxt as {ctxt, thy, stds, specialize, fast_descrs, def_table, - simp_table, special_funs, ...}) depth t = + simp_table, special_funs, ...}) def depth t = if not specialize orelse depth > special_max_depth then t else let - val blacklist = if depth = 0 then [] - else case term_under_def t of Const x => [x] | _ => [] + val blacklist = + if def then case term_under_def t of Const x => [x] | _ => [] else [] fun aux args Ts (Const (x as (s, T))) = ((if not (member (op =) blacklist x) andalso not (null args) andalso not (String.isPrefix special_prefix s) andalso @@ -901,21 +901,21 @@ List.partition (assumption_exclusively_defines_free assm_ts) assm_ts val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts type accumulator = styp list * (term list * term list) - fun add_axiom get app depth t (accum as (seen, axs)) = + fun add_axiom get app def depth t (accum as (seen, axs)) = let val t = t |> unfold_defs_in_term hol_ctxt - |> skolemize_term_and_more hol_ctxt ~1 (*### why ~1? *) + |> skolemize_term_and_more hol_ctxt ~1 (* FIXME: why ~1? *) in if is_trivial_equation t then accum else - let val t' = t |> specialize_consts_in_term hol_ctxt depth in + let val t' = t |> specialize_consts_in_term hol_ctxt def depth in if exists (member (op aconv) (get axs)) [t, t'] then accum else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs) end end - and add_def_axiom depth = add_axiom fst apfst depth - and add_nondef_axiom depth = add_axiom snd apsnd depth + and add_def_axiom depth = add_axiom fst apfst true depth + and add_nondef_axiom depth = add_axiom snd apsnd false depth and add_maybe_def_axiom depth t = (if head_of t <> @{const "==>"} then add_def_axiom else add_nondef_axiom) depth t @@ -1285,7 +1285,7 @@ neg_t |> unfold_defs_in_term hol_ctxt |> close_form |> skolemize_term_and_more hol_ctxt max_skolem_depth - |> specialize_consts_in_term hol_ctxt 0 + |> specialize_consts_in_term hol_ctxt false 0 |> axioms_for_term hol_ctxt assm_ts val binarize = is_standard_datatype thy stds nat_T andalso diff -r 37a7272cb453 -r 78403fcd0ec5 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Aug 05 14:45:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Aug 05 15:44:54 2010 +0200 @@ -64,7 +64,6 @@ -> typ val is_of_class_const : theory -> string * typ -> bool val get_class_def : theory -> string -> (string * term) option - val extensionalize_term : term -> term val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> string * typ -> term -> term val nat_subscript : int -> string @@ -251,7 +250,6 @@ val typ_of_dtyp = Refute.typ_of_dtyp val is_of_class_const = Refute.is_const_of_class val get_class_def = Refute.get_classdef -val extensionalize_term = Sledgehammer_Util.extensionalize_term val monomorphic_term = Sledgehammer_Util.monomorphic_term val specialize_type = Sledgehammer_Util.specialize_type