src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 40048 f3a46d524101
parent 39802 7cadad6a18cc
child 40049 75d9f57123d6
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Oct 20 21:26:51 2010 -0700
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:06 2010 +0200
     1.3 @@ -117,6 +117,7 @@
     1.4      no_higher_order_predicate : string list,
     1.5      inductify : bool,
     1.6      detect_switches : bool,
     1.7 +    smart_depth_limiting : bool,
     1.8      compilation : compilation
     1.9    };
    1.10    val expected_modes : options -> (string * mode list) option
    1.11 @@ -138,6 +139,7 @@
    1.12    val no_higher_order_predicate : options -> string list
    1.13    val is_inductify : options -> bool
    1.14    val detect_switches : options -> bool
    1.15 +  val smart_depth_limiting : options -> bool
    1.16    val compilation : options -> compilation
    1.17    val default_options : options
    1.18    val bool_options : string list
    1.19 @@ -729,6 +731,7 @@
    1.20    no_higher_order_predicate : string list,
    1.21    inductify : bool,
    1.22    detect_switches : bool,
    1.23 +  smart_depth_limiting : bool,
    1.24    compilation : compilation
    1.25  };
    1.26  
    1.27 @@ -759,6 +762,8 @@
    1.28  
    1.29  fun detect_switches (Options opt) = #detect_switches opt
    1.30  
    1.31 +fun smart_depth_limiting (Options opt) = #smart_depth_limiting opt
    1.32 +
    1.33  val default_options = Options {
    1.34    expected_modes = NONE,
    1.35    proposed_modes = [],
    1.36 @@ -779,12 +784,14 @@
    1.37    no_higher_order_predicate = [],
    1.38    inductify = false,
    1.39    detect_switches = true,
    1.40 +  smart_depth_limiting = false,
    1.41    compilation = Pred
    1.42  }
    1.43  
    1.44  val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
    1.45    "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
    1.46 -  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
    1.47 +  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering",
    1.48 +  "smart_depth_limiting"]
    1.49  
    1.50  fun print_step options s =
    1.51    if show_steps options then tracing s else ()