adding option smart_depth_limiting to predicate compiler
authorbulwahn
Thu Oct 21 19:13:06 2010 +0200 (2010-10-21)
changeset 40048f3a46d524101
parent 40047 6547d0f079ed
child 40049 75d9f57123d6
adding option smart_depth_limiting to predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Oct 20 21:26:51 2010 -0700
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Oct 21 19:13:06 2010 +0200
     1.3 @@ -173,6 +173,7 @@
     1.4        no_higher_order_predicate = [],
     1.5        inductify = chk "inductify",
     1.6        detect_switches = chk "detect_switches",
     1.7 +      smart_depth_limiting = chk "smart_depth_limiting",
     1.8        compilation = compilation
     1.9      }
    1.10    end
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Oct 20 21:26:51 2010 -0700
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:06 2010 +0200
     2.3 @@ -117,6 +117,7 @@
     2.4      no_higher_order_predicate : string list,
     2.5      inductify : bool,
     2.6      detect_switches : bool,
     2.7 +    smart_depth_limiting : bool,
     2.8      compilation : compilation
     2.9    };
    2.10    val expected_modes : options -> (string * mode list) option
    2.11 @@ -138,6 +139,7 @@
    2.12    val no_higher_order_predicate : options -> string list
    2.13    val is_inductify : options -> bool
    2.14    val detect_switches : options -> bool
    2.15 +  val smart_depth_limiting : options -> bool
    2.16    val compilation : options -> compilation
    2.17    val default_options : options
    2.18    val bool_options : string list
    2.19 @@ -729,6 +731,7 @@
    2.20    no_higher_order_predicate : string list,
    2.21    inductify : bool,
    2.22    detect_switches : bool,
    2.23 +  smart_depth_limiting : bool,
    2.24    compilation : compilation
    2.25  };
    2.26  
    2.27 @@ -759,6 +762,8 @@
    2.28  
    2.29  fun detect_switches (Options opt) = #detect_switches opt
    2.30  
    2.31 +fun smart_depth_limiting (Options opt) = #smart_depth_limiting opt
    2.32 +
    2.33  val default_options = Options {
    2.34    expected_modes = NONE,
    2.35    proposed_modes = [],
    2.36 @@ -779,12 +784,14 @@
    2.37    no_higher_order_predicate = [],
    2.38    inductify = false,
    2.39    detect_switches = true,
    2.40 +  smart_depth_limiting = false,
    2.41    compilation = Pred
    2.42  }
    2.43  
    2.44  val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
    2.45    "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
    2.46 -  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
    2.47 +  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering",
    2.48 +  "smart_depth_limiting"]
    2.49  
    2.50  fun print_step options s =
    2.51    if show_steps options then tracing s else ()