lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
authorblanchet
Wed Mar 02 14:50:16 2011 +0100 (2011-03-02)
changeset 41871394eef237bd1
parent 41870 a14a492f472f
child 41872 10fd9e5d58ba
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Mar 02 13:09:57 2011 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Mar 02 14:50:16 2011 +0100
     1.3 @@ -38,8 +38,8 @@
     1.4    {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
     1.5     stds = stds, wfs = [], user_axioms = NONE, debug = false,
     1.6     whacks = [], binary_ints = SOME false, destroy_constrs = true,
     1.7 -   specialize = false, star_linear_preds = false, preconstrs = [],
     1.8 -   tac_timeout = NONE, evals = [], case_names = case_names,
     1.9 +   specialize = false, star_linear_preds = false, total_consts = NONE,
    1.10 +   preconstrs = [], tac_timeout = NONE, evals = [], case_names = case_names,
    1.11     def_tables = def_tables, nondef_table = nondef_table,
    1.12     user_nondefs = user_nondefs, simp_table = simp_table,
    1.13     psimp_table = psimp_table, choice_spec_table = choice_spec_table,
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 14:50:16 2011 +0100
     2.3 @@ -288,14 +288,14 @@
     2.4         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
     2.5         whacks = whacks, binary_ints = binary_ints,
     2.6         destroy_constrs = destroy_constrs, specialize = specialize,
     2.7 -       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
     2.8 -       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
     2.9 -       def_tables = def_tables, nondef_table = nondef_table,
    2.10 -       user_nondefs = user_nondefs, simp_table = simp_table,
    2.11 -       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    2.12 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    2.13 -       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    2.14 -       special_funs = Unsynchronized.ref [],
    2.15 +       star_linear_preds = star_linear_preds, total_consts = total_consts,
    2.16 +       preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
    2.17 +       case_names = case_names, def_tables = def_tables,
    2.18 +       nondef_table = nondef_table, user_nondefs = user_nondefs,
    2.19 +       simp_table = simp_table, psimp_table = psimp_table,
    2.20 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    2.21 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    2.22 +       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    2.23         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    2.24         constr_cache = Unsynchronized.ref []}
    2.25      val pseudo_frees = []
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 13:09:57 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 14:50:16 2011 +0100
     3.3 @@ -27,6 +27,7 @@
     3.4       destroy_constrs: bool,
     3.5       specialize: bool,
     3.6       star_linear_preds: bool,
     3.7 +     total_consts: bool option,
     3.8       preconstrs: (term option * bool option) list,
     3.9       tac_timeout: Time.time option,
    3.10       evals: term list,
    3.11 @@ -259,6 +260,7 @@
    3.12     destroy_constrs: bool,
    3.13     specialize: bool,
    3.14     star_linear_preds: bool,
    3.15 +   total_consts: bool option,
    3.16     preconstrs: (term option * bool option) list,
    3.17     tac_timeout: Time.time option,
    3.18     evals: term list,
    3.19 @@ -1634,13 +1636,15 @@
    3.20  val unfold_max_depth = 255
    3.21  
    3.22  (* Inline definitions or define as an equational constant? Booleans tend to
    3.23 -   benefit more from inlining, due to the polarity analysis. *)
    3.24 +   benefit more from inlining, due to the polarity analysis. (However, if
    3.25 +   "total_consts" is set, the polarity analysis is likely not to be so
    3.26 +   crucial.) *)
    3.27  val def_inline_threshold_for_booleans = 60
    3.28  val def_inline_threshold_for_non_booleans = 20
    3.29  
    3.30  fun unfold_defs_in_term
    3.31 -        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
    3.32 -                      ground_thm_table, ersatz_table, ...}) =
    3.33 +        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
    3.34 +                      def_tables, ground_thm_table, ersatz_table, ...}) =
    3.35    let
    3.36      fun do_term depth Ts t =
    3.37        case t of
    3.38 @@ -1718,7 +1722,8 @@
    3.39        | NONE =>
    3.40          let
    3.41            fun def_inline_threshold () =
    3.42 -            if is_boolean_type (nth_range_type (length ts) T) then
    3.43 +            if is_boolean_type (nth_range_type (length ts) T) andalso
    3.44 +               total_consts <> SOME true then
    3.45                def_inline_threshold_for_booleans
    3.46              else
    3.47                def_inline_threshold_for_non_booleans
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 13:09:57 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 02 14:50:16 2011 +0100
     4.3 @@ -862,8 +862,8 @@
     4.4  fun reconstruct_hol_model {show_datatypes, show_consts}
     4.5          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
     4.6                        debug, whacks, binary_ints, destroy_constrs, specialize,
     4.7 -                      star_linear_preds, preconstrs, tac_timeout, evals,
     4.8 -                      case_names, def_tables, nondef_table, user_nondefs,
     4.9 +                      star_linear_preds, total_consts, preconstrs, tac_timeout,
    4.10 +                      evals, case_names, def_tables, nondef_table, user_nondefs,
    4.11                        simp_table, psimp_table, choice_spec_table, intro_table,
    4.12                        ground_thm_table, ersatz_table, skolems, special_funs,
    4.13                        unrolled_preds, wf_cache, constr_cache}, binarize,
    4.14 @@ -879,15 +879,16 @@
    4.15         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    4.16         whacks = whacks, binary_ints = binary_ints,
    4.17         destroy_constrs = destroy_constrs, specialize = specialize,
    4.18 -       star_linear_preds = star_linear_preds, preconstrs = preconstrs,
    4.19 -       tac_timeout = tac_timeout, evals = evals, case_names = case_names,
    4.20 -       def_tables = def_tables, nondef_table = nondef_table,
    4.21 -       user_nondefs = user_nondefs, simp_table = simp_table,
    4.22 -       psimp_table = psimp_table, choice_spec_table = choice_spec_table,
    4.23 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    4.24 -       ersatz_table = ersatz_table, skolems = skolems,
    4.25 -       special_funs = special_funs, unrolled_preds = unrolled_preds,
    4.26 -       wf_cache = wf_cache, constr_cache = constr_cache}
    4.27 +       star_linear_preds = star_linear_preds, total_consts = total_consts,
    4.28 +       preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals,
    4.29 +       case_names = case_names, def_tables = def_tables,
    4.30 +       nondef_table = nondef_table, user_nondefs = user_nondefs,
    4.31 +       simp_table = simp_table, psimp_table = psimp_table,
    4.32 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    4.33 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    4.34 +       skolems = skolems, special_funs = special_funs,
    4.35 +       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    4.36 +       constr_cache = constr_cache}
    4.37      val scope =
    4.38        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    4.39         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}