fiddle with specialization etc.
--- 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 ()))
--- 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
--- 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