src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
author wenzelm
Sun Mar 20 21:28:11 2011 +0100 (2011-03-20 ago)
changeset 42012 2c3fe3cbebae
parent 41472 f6ab14e61604
child 42014 75417ef605ba
permissions -rw-r--r--
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@33250
     3
wenzelm@33265
     4
A quickcheck generator based on the predicate compiler.
bulwahn@33250
     5
*)
bulwahn@33250
     6
bulwahn@33250
     7
signature PREDICATE_COMPILE_QUICKCHECK =
bulwahn@33250
     8
sig
bulwahn@35324
     9
  (*val quickcheck : Proof.context -> term -> int -> term list option*)
haftmann@39388
    10
  val put_pred_result :
haftmann@39388
    11
    (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
haftmann@39388
    12
      Proof.context -> Proof.context;
haftmann@39388
    13
  val put_dseq_result :
haftmann@39388
    14
    (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
haftmann@39388
    15
      Proof.context -> Proof.context;
haftmann@39388
    16
  val put_lseq_result :
haftmann@39388
    17
    (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
haftmann@39388
    18
      Proof.context -> Proof.context;
bulwahn@40103
    19
  val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
bulwahn@40103
    20
    Proof.context -> Proof.context
bulwahn@36025
    21
bulwahn@34948
    22
  val tracing : bool Unsynchronized.ref;
bulwahn@36025
    23
  val quiet : bool Unsynchronized.ref;
bulwahn@36025
    24
  val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
bulwahn@40924
    25
    Proof.context -> term -> int -> term list option * Quickcheck.report option;
bulwahn@35324
    26
(*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
bulwahn@35324
    27
  val nrandom : int Unsynchronized.ref;
bulwahn@35324
    28
  val debug : bool Unsynchronized.ref;
bulwahn@35324
    29
  val function_flattening : bool Unsynchronized.ref;
bulwahn@35324
    30
  val no_higher_order_predicate : string list Unsynchronized.ref;
bulwahn@33250
    31
end;
bulwahn@33250
    32
bulwahn@33250
    33
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
bulwahn@33250
    34
struct
bulwahn@33250
    35
bulwahn@33257
    36
open Predicate_Compile_Aux;
bulwahn@33257
    37
wenzelm@41472
    38
(* FIXME just one data slot (record) per program unit *)
wenzelm@41472
    39
wenzelm@41472
    40
structure Pred_Result = Proof_Data
wenzelm@41472
    41
(
haftmann@39388
    42
  type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
wenzelm@41472
    43
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    44
  fun init _ () = error "Pred_Result"
haftmann@39388
    45
);
haftmann@39388
    46
val put_pred_result = Pred_Result.put;
bulwahn@34948
    47
wenzelm@41472
    48
structure Dseq_Result = Proof_Data
wenzelm@41472
    49
(
haftmann@39388
    50
  type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
wenzelm@41472
    51
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    52
  fun init _ () = error "Dseq_Result"
haftmann@39388
    53
);
haftmann@39388
    54
val put_dseq_result = Dseq_Result.put;
bulwahn@36025
    55
wenzelm@41472
    56
structure Lseq_Result = Proof_Data
wenzelm@41472
    57
(
haftmann@39388
    58
  type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
wenzelm@41472
    59
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    60
  fun init _ () = error "Lseq_Result"
haftmann@39388
    61
);
haftmann@39388
    62
val put_lseq_result = Lseq_Result.put;
bulwahn@36025
    63
wenzelm@41472
    64
structure New_Dseq_Result = Proof_Data
wenzelm@41472
    65
(
bulwahn@40103
    66
  type T = unit -> int -> term list Lazy_Sequence.lazy_sequence
wenzelm@41472
    67
  (* FIXME avoid user error with non-user text *)
bulwahn@40103
    68
  fun init _ () = error "New_Dseq_Random_Result"
bulwahn@40103
    69
);
bulwahn@40103
    70
val put_new_dseq_result = New_Dseq_Result.put;
bulwahn@40103
    71
bulwahn@34948
    72
val tracing = Unsynchronized.ref false;
bulwahn@33250
    73
bulwahn@35537
    74
val quiet = Unsynchronized.ref true;
bulwahn@33250
    75
bulwahn@35537
    76
val target = "Quickcheck"
bulwahn@35324
    77
bulwahn@36025
    78
val nrandom = Unsynchronized.ref 3;
bulwahn@35324
    79
bulwahn@35537
    80
val debug = Unsynchronized.ref false;
bulwahn@35324
    81
bulwahn@35324
    82
val function_flattening = Unsynchronized.ref true;
bulwahn@35324
    83
bulwahn@35538
    84
val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
bulwahn@35324
    85
bulwahn@33257
    86
val options = Options {
bulwahn@33257
    87
  expected_modes = NONE,
bulwahn@39382
    88
  proposed_modes = [],
bulwahn@33651
    89
  proposed_names = [],
bulwahn@35324
    90
  show_steps = false,
bulwahn@35324
    91
  show_intermediate_results = false,
bulwahn@35324
    92
  show_proof_trace = false,
bulwahn@35324
    93
  show_modes = false,
bulwahn@35324
    94
  show_mode_inference = false,
bulwahn@35324
    95
  show_compilation = false,
bulwahn@35324
    96
  show_caught_failures = false,
bulwahn@39383
    97
  show_invalid_clauses = false, 
bulwahn@35324
    98
  skip_proof = false,
bulwahn@35324
    99
  compilation = Random,
bulwahn@35324
   100
  inductify = true,
bulwahn@36256
   101
  specialise = true,
bulwahn@36256
   102
  detect_switches = false,
bulwahn@35324
   103
  function_flattening = true,
bulwahn@35324
   104
  fail_safe_function_flattening = false,
bulwahn@35324
   105
  no_higher_order_predicate = [],
bulwahn@40054
   106
  smart_depth_limiting = true,
bulwahn@36250
   107
  no_topmost_reordering = false
bulwahn@35324
   108
}
bulwahn@35324
   109
bulwahn@35324
   110
val debug_options = Options {
bulwahn@35324
   111
  expected_modes = NONE,
bulwahn@39383
   112
  proposed_modes = [],
bulwahn@35324
   113
  proposed_names = [],
bulwahn@33257
   114
  show_steps = true,
bulwahn@33257
   115
  show_intermediate_results = true,
bulwahn@33257
   116
  show_proof_trace = false,
bulwahn@35324
   117
  show_modes = true,
bulwahn@35324
   118
  show_mode_inference = true,
bulwahn@34948
   119
  show_compilation = false,
bulwahn@35324
   120
  show_caught_failures = true,
bulwahn@39383
   121
  show_invalid_clauses = false,
bulwahn@33257
   122
  skip_proof = false,
bulwahn@34948
   123
  compilation = Random,
bulwahn@35324
   124
  inductify = true,
bulwahn@36256
   125
  specialise = true,
bulwahn@36256
   126
  detect_switches = false,
bulwahn@35324
   127
  function_flattening = true,
bulwahn@35324
   128
  fail_safe_function_flattening = false,
bulwahn@35324
   129
  no_higher_order_predicate = [],
bulwahn@40054
   130
  smart_depth_limiting = true,
bulwahn@35324
   131
  no_topmost_reordering = true
bulwahn@33257
   132
}
bulwahn@33257
   133
bulwahn@35324
   134
bulwahn@35324
   135
fun set_function_flattening b
bulwahn@35324
   136
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   137
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   138
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   139
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   140
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
bulwahn@35324
   141
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   142
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   143
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   144
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   145
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   146
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   147
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
bulwahn@35324
   148
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   149
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   150
bulwahn@35324
   151
fun set_fail_safe_function_flattening b
bulwahn@35324
   152
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   153
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   154
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   155
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   156
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
bulwahn@35324
   157
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   158
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   159
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   160
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   161
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   162
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   163
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
bulwahn@35324
   164
    fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
bulwahn@40054
   165
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   166
bulwahn@35324
   167
fun set_no_higher_order_predicate ss
bulwahn@35324
   168
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   169
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   170
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   171
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   172
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
bulwahn@35324
   173
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   174
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   175
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   176
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   177
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   178
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   179
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
bulwahn@40054
   180
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss,
bulwahn@40054
   181
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   182
bulwahn@35324
   183
bulwahn@35324
   184
fun get_options () = 
bulwahn@35324
   185
  set_no_higher_order_predicate (!no_higher_order_predicate)
bulwahn@35324
   186
    (set_function_flattening (!function_flattening)
bulwahn@35324
   187
      (if !debug then debug_options else options))
bulwahn@35324
   188
bulwahn@36046
   189
val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
bulwahn@36046
   190
val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
bulwahn@36046
   191
val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
bulwahn@36025
   192
bulwahn@36046
   193
val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
bulwahn@36046
   194
val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
bulwahn@36046
   195
val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
bulwahn@33250
   196
bulwahn@40054
   197
val mk_new_randompredT =
bulwahn@40103
   198
  Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40054
   199
val mk_new_return =
bulwahn@40103
   200
  Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40054
   201
val mk_new_bind =
bulwahn@40103
   202
  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   203
bulwahn@40103
   204
val mk_new_dseqT =
bulwahn@40103
   205
  Predicate_Compile_Aux.mk_predT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   206
val mk_gen_return =
bulwahn@40103
   207
  Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   208
val mk_gen_bind =
bulwahn@40103
   209
  Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   210
  
bulwahn@36025
   211
krauss@39756
   212
val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
bulwahn@33250
   213
wenzelm@42012
   214
fun cpu_time description f =  (* FIXME !? *)
bulwahn@33250
   215
  let
wenzelm@42012
   216
    val start = Timing.start ()
bulwahn@35324
   217
    val result = Exn.capture f ()
wenzelm@42012
   218
    val time = Time.toMilliseconds (#cpu (Timing.result start))
bulwahn@35324
   219
  in (Exn.release result, (description, time)) end
bulwahn@35324
   220
bulwahn@36025
   221
fun compile_term compilation options ctxt t =
bulwahn@35324
   222
  let
wenzelm@38755
   223
    val thy = Theory.copy (ProofContext.theory_of ctxt)
bulwahn@39541
   224
    val ((((full_constname, constT), vs'), intro), thy1) =
bulwahn@39541
   225
      Predicate_Compile_Aux.define_quickcheck_predicate t thy
bulwahn@35324
   226
    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
bulwahn@36256
   227
    val (thy3, preproc_time) = cpu_time "predicate preprocessing"
bulwahn@39541
   228
        (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
bulwahn@35324
   229
    val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
bulwahn@36025
   230
        (fn () =>
bulwahn@36025
   231
          case compilation of
bulwahn@36025
   232
            Pos_Random_DSeq =>
bulwahn@36025
   233
              Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3
bulwahn@36025
   234
          | New_Pos_Random_DSeq =>
bulwahn@36025
   235
              Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
bulwahn@40103
   236
          | Pos_Generator_DSeq =>
bulwahn@40103
   237
              Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
bulwahn@36025
   238
          (*| Depth_Limited_Random =>
bulwahn@36025
   239
              Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
bulwahn@36256
   240
    (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
bulwahn@36256
   241
    val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
bulwahn@36256
   242
    val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
bulwahn@37005
   243
    val ctxt4 = ProofContext.init_global thy4
bulwahn@40054
   244
    val modes = Core_Data.modes_of compilation ctxt4 full_constname
bulwahn@34948
   245
    val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
bulwahn@33250
   246
    val prog =
bulwahn@34948
   247
      if member eq_mode modes output_mode then
bulwahn@33250
   248
        let
bulwahn@40054
   249
          val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
bulwahn@36025
   250
          val T = 
bulwahn@36025
   251
            case compilation of
bulwahn@36025
   252
              Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@36025
   253
            | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@40103
   254
            | Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@36025
   255
            | Depth_Limited_Random =>
bulwahn@36025
   256
              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
bulwahn@36025
   257
              @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@34948
   258
        in
bulwahn@34948
   259
          Const (name, T)
bulwahn@34948
   260
        end
bulwahn@35324
   261
      else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
bulwahn@36025
   262
    val qc_term =
bulwahn@36025
   263
      case compilation of
bulwahn@36025
   264
          Pos_Random_DSeq => mk_bind (prog,
bulwahn@36025
   265
            mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
bulwahn@36025
   266
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@36025
   267
        | New_Pos_Random_DSeq => mk_new_bind (prog,
bulwahn@36025
   268
            mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
bulwahn@36025
   269
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@40103
   270
        | Pos_Generator_DSeq => mk_gen_bind (prog,
bulwahn@40103
   271
            mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
bulwahn@40103
   272
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@36025
   273
        | Depth_Limited_Random => fold_rev (curry absdummy)
bulwahn@36025
   274
            [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
bulwahn@36025
   275
             @{typ "code_numeral * code_numeral"}]
bulwahn@36025
   276
            (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
bulwahn@36025
   277
            mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
bulwahn@36025
   278
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
bulwahn@36025
   279
    val prog =
bulwahn@36025
   280
      case compilation of
bulwahn@36025
   281
        Pos_Random_DSeq =>
bulwahn@36025
   282
          let
bulwahn@36025
   283
            val compiled_term =
haftmann@39471
   284
              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
haftmann@39471
   285
                thy4 (SOME target)
bulwahn@36025
   286
                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
haftmann@39471
   287
                qc_term []
bulwahn@36025
   288
          in
bulwahn@36025
   289
            (fn size => fn nrandom => fn depth =>
bulwahn@36025
   290
              Option.map fst (DSequence.yield
bulwahn@36025
   291
                (compiled_term nrandom size |> Random_Engine.run) depth true))
bulwahn@36025
   292
          end
bulwahn@36025
   293
      | New_Pos_Random_DSeq =>
bulwahn@36025
   294
          let
bulwahn@36025
   295
            val compiled_term =
haftmann@39471
   296
              Code_Runtime.dynamic_value_strict
haftmann@39388
   297
                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
haftmann@39471
   298
                thy4 (SOME target)
bulwahn@36025
   299
                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
haftmann@36533
   300
                  g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
haftmann@39471
   301
                  qc_term []
bulwahn@36025
   302
          in
bulwahn@36025
   303
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
bulwahn@36025
   304
               (
bulwahn@36025
   305
               let
bulwahn@36025
   306
                 val seed = Random_Engine.next_seed ()
bulwahn@36025
   307
               in compiled_term nrandom size seed depth end))
bulwahn@36025
   308
          end
bulwahn@40103
   309
      | Pos_Generator_DSeq =>
bulwahn@40103
   310
          let
bulwahn@40103
   311
            val compiled_term =
bulwahn@40103
   312
              Code_Runtime.dynamic_value_strict
bulwahn@40103
   313
                (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
bulwahn@40103
   314
                thy4 (SOME target)
bulwahn@40103
   315
                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.mapa o map) proc)
bulwahn@40103
   316
                qc_term []
bulwahn@40103
   317
          in
bulwahn@40103
   318
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
bulwahn@40103
   319
          end
bulwahn@40103
   320
       | Depth_Limited_Random =>
bulwahn@36025
   321
          let
haftmann@39471
   322
            val compiled_term = Code_Runtime.dynamic_value_strict
haftmann@39388
   323
              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
haftmann@39471
   324
                thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
bulwahn@36025
   325
                  g depth nrandom size seed |> (Predicate.map o map) proc)
haftmann@39471
   326
                qc_term []
bulwahn@36025
   327
          in
bulwahn@36025
   328
            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
bulwahn@36025
   329
              (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
bulwahn@36025
   330
          end
bulwahn@33250
   331
  in
bulwahn@36025
   332
    prog
bulwahn@35324
   333
  end
bulwahn@35324
   334
bulwahn@35324
   335
fun try_upto quiet f i =
bulwahn@35324
   336
  let
bulwahn@35324
   337
    fun try' j =
bulwahn@35324
   338
      if j <= i then
bulwahn@35324
   339
        let
wenzelm@40132
   340
          val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
bulwahn@35324
   341
        in
bulwahn@35324
   342
          case f j handle Match => (if quiet then ()
bulwahn@35324
   343
             else warning "Exception Match raised during quickcheck"; NONE)
bulwahn@35324
   344
          of NONE => try' (j + 1) | SOME q => SOME q
bulwahn@35324
   345
        end
bulwahn@35324
   346
      else
bulwahn@35324
   347
        NONE
bulwahn@35324
   348
  in
bulwahn@35324
   349
    try' 0
bulwahn@35324
   350
  end
bulwahn@35324
   351
bulwahn@35324
   352
(* quickcheck interface functions *)
bulwahn@35324
   353
bulwahn@39253
   354
fun compile_term' compilation options depth ctxt t =
bulwahn@35324
   355
  let
bulwahn@36025
   356
    val c = compile_term compilation options ctxt t
bulwahn@35324
   357
  in
bulwahn@40924
   358
    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
bulwahn@35324
   359
  end
bulwahn@35324
   360
bulwahn@36025
   361
fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
bulwahn@35324
   362
  let
bulwahn@35324
   363
     val options =
bulwahn@35324
   364
       set_fail_safe_function_flattening fail_safe_function_flattening
bulwahn@35324
   365
         (set_function_flattening function_flattening (get_options ()))
bulwahn@35324
   366
  in
bulwahn@36025
   367
    compile_term' compilation options depth
bulwahn@33250
   368
  end
bulwahn@33250
   369
bulwahn@33250
   370
end;