# HG changeset patch
# User blanchet
# Date 1426453215 -3600
# Node ID 4aa63424ba89ccaf21c2557a80c6ae14f548ae67
# Parent  44dabb962e481061e43be29c019a3fc9ce8f9791
inlining threshold

diff -r 44dabb962e48 -r 4aa63424ba89 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 15 22:00:15 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Mar 15 22:00:15 2015 +0100
@@ -8,6 +8,8 @@
 
 signature BNF_COMP =
 sig
+  val bnf_inline_threshold: int Config.T
+
   val ID_bnf: BNF_Def.bnf
   val DEADID_bnf: BNF_Def.bnf
 
@@ -54,6 +56,8 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
+val bnf_inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
+
 val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
 val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
 
@@ -730,12 +734,12 @@
 val mk_abs = mk_abs_or_rep range_type;
 val mk_rep = mk_abs_or_rep domain_type;
 
-val smart_max_inline_type_size = 5; (*FUDGE*)
-
-fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac =
+fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
   let
+    val threshold = Config.get ctxt bnf_inline_threshold;
     val repT = HOLogic.dest_setT (fastype_of set);
-    val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size;
+    val out_of_line = force_out_of_line orelse
+      (threshold >= 0 andalso Term.size_of_typ repT > threshold);
   in
     if out_of_line then
       typedef (b, As, mx) set opt_morphs tac
@@ -769,7 +773,7 @@
     val T_bind = qualify b;
     val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
     val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
-      maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
+      maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
         (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
     val repTB = mk_T_of_bnf Ds Bs bnf;
@@ -799,7 +803,7 @@
     val all_deads = map TFree (fold Term.add_tfreesT Ds []);
 
     val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
-      maybe_typedef false (bdT_bind, params, NoSyn)
+      maybe_typedef lthy false (bdT_bind, params, NoSyn)
         (HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
     val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =