src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41871 394eef237bd1
parent 41860 49d0fc8c418c
child 41875 e3cd0dce9b1a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 13:09:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 14:50:16 2011 +0100
     1.3 @@ -27,6 +27,7 @@
     1.4       destroy_constrs: bool,
     1.5       specialize: bool,
     1.6       star_linear_preds: bool,
     1.7 +     total_consts: bool option,
     1.8       preconstrs: (term option * bool option) list,
     1.9       tac_timeout: Time.time option,
    1.10       evals: term list,
    1.11 @@ -259,6 +260,7 @@
    1.12     destroy_constrs: bool,
    1.13     specialize: bool,
    1.14     star_linear_preds: bool,
    1.15 +   total_consts: bool option,
    1.16     preconstrs: (term option * bool option) list,
    1.17     tac_timeout: Time.time option,
    1.18     evals: term list,
    1.19 @@ -1634,13 +1636,15 @@
    1.20  val unfold_max_depth = 255
    1.21  
    1.22  (* Inline definitions or define as an equational constant? Booleans tend to
    1.23 -   benefit more from inlining, due to the polarity analysis. *)
    1.24 +   benefit more from inlining, due to the polarity analysis. (However, if
    1.25 +   "total_consts" is set, the polarity analysis is likely not to be so
    1.26 +   crucial.) *)
    1.27  val def_inline_threshold_for_booleans = 60
    1.28  val def_inline_threshold_for_non_booleans = 20
    1.29  
    1.30  fun unfold_defs_in_term
    1.31 -        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
    1.32 -                      ground_thm_table, ersatz_table, ...}) =
    1.33 +        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
    1.34 +                      def_tables, ground_thm_table, ersatz_table, ...}) =
    1.35    let
    1.36      fun do_term depth Ts t =
    1.37        case t of
    1.38 @@ -1718,7 +1722,8 @@
    1.39        | NONE =>
    1.40          let
    1.41            fun def_inline_threshold () =
    1.42 -            if is_boolean_type (nth_range_type (length ts) T) then
    1.43 +            if is_boolean_type (nth_range_type (length ts) T) andalso
    1.44 +               total_consts <> SOME true then
    1.45                def_inline_threshold_for_booleans
    1.46              else
    1.47                def_inline_threshold_for_non_booleans