src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 36254 95ef0a3cf31c
parent 36251 5fd5d732a4ea
child 36610 bafd82950e24
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    datatype indprem = Prem of term | Negprem of term | Sidecond of term
     1.5      | Generator of (string * typ)
     1.6    val dest_indprem : indprem -> term
     1.7 +  val map_indprem : (term -> term) -> indprem -> indprem
     1.8    (* general syntactic functions *)
     1.9    val conjuncts : term -> term list
    1.10    val is_equationlike : thm -> bool
    1.11 @@ -111,6 +112,7 @@
    1.12      specialise : bool,
    1.13      no_higher_order_predicate : string list,
    1.14      inductify : bool,
    1.15 +    detect_switches : bool,
    1.16      compilation : compilation
    1.17    };
    1.18    val expected_modes : options -> (string * mode list) option
    1.19 @@ -130,6 +132,7 @@
    1.20    val specialise : options -> bool
    1.21    val no_higher_order_predicate : options -> string list
    1.22    val is_inductify : options -> bool
    1.23 +  val detect_switches : options -> bool
    1.24    val compilation : options -> compilation
    1.25    val default_options : options
    1.26    val bool_options : string list
    1.27 @@ -394,6 +397,11 @@
    1.28    | dest_indprem (Sidecond t) = t
    1.29    | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
    1.30  
    1.31 +fun map_indprem f (Prem t) = Prem (f t)
    1.32 +  | map_indprem f (Negprem t) = Negprem (f t)
    1.33 +  | map_indprem f (Sidecond t) = Sidecond (f t)
    1.34 +  | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
    1.35 +
    1.36  (* general syntactic functions *)
    1.37  
    1.38  (*Like dest_conj, but flattens conjunctions however nested*)
    1.39 @@ -677,6 +685,7 @@
    1.40    fail_safe_function_flattening : bool,
    1.41    no_higher_order_predicate : string list,
    1.42    inductify : bool,
    1.43 +  detect_switches : bool,
    1.44    compilation : compilation
    1.45  };
    1.46  
    1.47 @@ -705,6 +714,8 @@
    1.48  
    1.49  fun compilation (Options opt) = #compilation opt
    1.50  
    1.51 +fun detect_switches (Options opt) = #detect_switches opt
    1.52 +
    1.53  val default_options = Options {
    1.54    expected_modes = NONE,
    1.55    proposed_modes = NONE,
    1.56 @@ -723,12 +734,13 @@
    1.57    fail_safe_function_flattening = false,
    1.58    no_higher_order_predicate = [],
    1.59    inductify = false,
    1.60 +  detect_switches = true,
    1.61    compilation = Pred
    1.62  }
    1.63  
    1.64  val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
    1.65    "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
    1.66 -  "specialise", "no_topmost_reordering"]
    1.67 +  "detect_switches", "specialise", "no_topmost_reordering"]
    1.68  
    1.69  fun print_step options s =
    1.70    if show_steps options then tracing s else ()