# HG changeset patch
# User blanchet
# Date 1299073816 -3600
# Node ID 394eef237bd109c3568bc7ae07384fb4a9edfb84
# Parent  a14a492f472f11f84ea79333c47f4d431100c756
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on

diff -r a14a492f472f -r 394eef237bd1 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Mar 02 14:50:16 2011 +0100
@@ -38,8 +38,8 @@
   {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
    stds = stds, wfs = [], user_axioms = NONE, debug = false,
    whacks = [], binary_ints = SOME false, destroy_constrs = true,
-   specialize = false, star_linear_preds = false, preconstrs = [],
-   tac_timeout = NONE, evals = [], case_names = case_names,
+   specialize = false, star_linear_preds = false, total_consts = NONE,
+   preconstrs = [], tac_timeout = NONE, 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,
diff -r a14a492f472f -r 394eef237bd1 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 14:50:16 2011 +0100
@@ -288,14 +288,14 @@
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        whacks = whacks, binary_ints = binary_ints,
        destroy_constrs = destroy_constrs, specialize = specialize,
-       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
-       tac_timeout = tac_timeout, 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, ground_thm_table = ground_thm_table,
-       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
-       special_funs = Unsynchronized.ref [],
+       star_linear_preds = star_linear_preds, total_consts = total_consts,
+       preconstrs = preconstrs, tac_timeout = tac_timeout, 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,
+       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
     val pseudo_frees = []
diff -r a14a492f472f -r 394eef237bd1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 14:50:16 2011 +0100
@@ -27,6 +27,7 @@
      destroy_constrs: bool,
      specialize: bool,
      star_linear_preds: bool,
+     total_consts: bool option,
      preconstrs: (term option * bool option) list,
      tac_timeout: Time.time option,
      evals: term list,
@@ -259,6 +260,7 @@
    destroy_constrs: bool,
    specialize: bool,
    star_linear_preds: bool,
+   total_consts: bool option,
    preconstrs: (term option * bool option) list,
    tac_timeout: Time.time option,
    evals: term list,
@@ -1634,13 +1636,15 @@
 val unfold_max_depth = 255
 
 (* Inline definitions or define as an equational constant? Booleans tend to
-   benefit more from inlining, due to the polarity analysis. *)
+   benefit more from inlining, due to the polarity analysis. (However, if
+   "total_consts" is set, the polarity analysis is likely not to be so
+   crucial.) *)
 val def_inline_threshold_for_booleans = 60
 val def_inline_threshold_for_non_booleans = 20
 
 fun unfold_defs_in_term
-        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
-                      ground_thm_table, ersatz_table, ...}) =
+        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
+                      def_tables, ground_thm_table, ersatz_table, ...}) =
   let
     fun do_term depth Ts t =
       case t of
@@ -1718,7 +1722,8 @@
       | NONE =>
         let
           fun def_inline_threshold () =
-            if is_boolean_type (nth_range_type (length ts) T) then
+            if is_boolean_type (nth_range_type (length ts) T) andalso
+               total_consts <> SOME true then
               def_inline_threshold_for_booleans
             else
               def_inline_threshold_for_non_booleans
diff -r a14a492f472f -r 394eef237bd1 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 14:50:16 2011 +0100
@@ -862,8 +862,8 @@
 fun reconstruct_hol_model {show_datatypes, show_consts}
         ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
                       debug, whacks, binary_ints, destroy_constrs, specialize,
-                      star_linear_preds, preconstrs, tac_timeout, evals,
-                      case_names, def_tables, nondef_table, user_nondefs,
+                      star_linear_preds, total_consts, preconstrs, tac_timeout,
+                      evals, case_names, 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}, binarize,
@@ -879,15 +879,16 @@
        stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
        whacks = whacks, binary_ints = binary_ints,
        destroy_constrs = destroy_constrs, specialize = specialize,
-       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
-       tac_timeout = tac_timeout, 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, ground_thm_table = ground_thm_table,
-       ersatz_table = ersatz_table, skolems = skolems,
-       special_funs = special_funs, unrolled_preds = unrolled_preds,
-       wf_cache = wf_cache, constr_cache = constr_cache}
+       star_linear_preds = star_linear_preds, total_consts = total_consts,
+       preconstrs = preconstrs, tac_timeout = tac_timeout, 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,
+       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
+       skolems = skolems, special_funs = special_funs,
+       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
+       constr_cache = constr_cache}
     val scope =
       {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
        bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}