src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
author haftmann
Fri Feb 15 08:31:31 2013 +0100 (2013-02-15)
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 52788 da1fdbfebd39
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
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
haftmann@50057
     9
  type seed = Random_Engine.seed
bulwahn@35324
    10
  (*val quickcheck : Proof.context -> term -> int -> term list option*)
haftmann@39388
    11
  val put_pred_result :
haftmann@51143
    12
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred) ->
haftmann@39388
    13
      Proof.context -> Proof.context;
haftmann@39388
    14
  val put_dseq_result :
haftmann@51143
    15
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed) ->
haftmann@39388
    16
      Proof.context -> Proof.context;
haftmann@39388
    17
  val put_lseq_result :
haftmann@51143
    18
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
haftmann@39388
    19
      Proof.context -> Proof.context;
haftmann@51143
    20
  val put_new_dseq_result : (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
bulwahn@40103
    21
    Proof.context -> Proof.context
haftmann@51143
    22
  val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) ->
bulwahn@45450
    23
    Proof.context -> Proof.context
bulwahn@45450
    24
  val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
bulwahn@43886
    25
    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
bulwahn@43886
    26
      -> Quickcheck.result list
bulwahn@35324
    27
  val nrandom : int Unsynchronized.ref;
bulwahn@35324
    28
  val debug : bool Unsynchronized.ref;
bulwahn@35324
    29
  val no_higher_order_predicate : string list Unsynchronized.ref;
bulwahn@43886
    30
  val setup : theory -> theory
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
haftmann@50093
    38
type seed = Random_Engine.seed;
haftmann@50057
    39
wenzelm@41472
    40
(* FIXME just one data slot (record) per program unit *)
wenzelm@41472
    41
wenzelm@41472
    42
structure Pred_Result = Proof_Data
wenzelm@41472
    43
(
haftmann@51143
    44
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
wenzelm@41472
    45
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    46
  fun init _ () = error "Pred_Result"
haftmann@39388
    47
);
haftmann@39388
    48
val put_pred_result = Pred_Result.put;
bulwahn@34948
    49
wenzelm@41472
    50
structure Dseq_Result = Proof_Data
wenzelm@41472
    51
(
haftmann@51143
    52
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
wenzelm@41472
    53
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    54
  fun init _ () = error "Dseq_Result"
haftmann@39388
    55
);
haftmann@39388
    56
val put_dseq_result = Dseq_Result.put;
bulwahn@36025
    57
wenzelm@41472
    58
structure Lseq_Result = Proof_Data
wenzelm@41472
    59
(
haftmann@51143
    60
  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
wenzelm@41472
    61
  (* FIXME avoid user error with non-user text *)
haftmann@39388
    62
  fun init _ () = error "Lseq_Result"
haftmann@39388
    63
);
haftmann@39388
    64
val put_lseq_result = Lseq_Result.put;
bulwahn@36025
    65
wenzelm@41472
    66
structure New_Dseq_Result = Proof_Data
wenzelm@41472
    67
(
haftmann@51143
    68
  type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
wenzelm@41472
    69
  (* FIXME avoid user error with non-user text *)
bulwahn@40103
    70
  fun init _ () = error "New_Dseq_Random_Result"
bulwahn@40103
    71
);
bulwahn@40103
    72
val put_new_dseq_result = New_Dseq_Result.put;
bulwahn@40103
    73
bulwahn@45450
    74
structure CPS_Result = Proof_Data
bulwahn@45450
    75
(
haftmann@51143
    76
  type T = unit -> Code_Numeral.natural -> (bool * term list) option
bulwahn@45450
    77
  (* FIXME avoid user error with non-user text *)
bulwahn@45450
    78
  fun init _ () = error "CPS_Result"
bulwahn@45450
    79
);
bulwahn@45450
    80
val put_cps_result = CPS_Result.put;
bulwahn@45450
    81
bulwahn@35537
    82
val target = "Quickcheck"
bulwahn@35324
    83
bulwahn@36025
    84
val nrandom = Unsynchronized.ref 3;
bulwahn@35324
    85
bulwahn@35537
    86
val debug = Unsynchronized.ref false;
bulwahn@35324
    87
bulwahn@35538
    88
val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
bulwahn@35324
    89
bulwahn@33257
    90
val options = Options {
bulwahn@33257
    91
  expected_modes = NONE,
bulwahn@39382
    92
  proposed_modes = [],
bulwahn@33651
    93
  proposed_names = [],
bulwahn@35324
    94
  show_steps = false,
bulwahn@35324
    95
  show_intermediate_results = false,
bulwahn@35324
    96
  show_proof_trace = false,
bulwahn@35324
    97
  show_modes = false,
bulwahn@35324
    98
  show_mode_inference = false,
bulwahn@35324
    99
  show_compilation = false,
bulwahn@35324
   100
  show_caught_failures = false,
bulwahn@39383
   101
  show_invalid_clauses = false, 
bulwahn@35324
   102
  skip_proof = false,
bulwahn@35324
   103
  compilation = Random,
bulwahn@35324
   104
  inductify = true,
bulwahn@36256
   105
  specialise = true,
bulwahn@36256
   106
  detect_switches = false,
bulwahn@35324
   107
  function_flattening = true,
bulwahn@35324
   108
  fail_safe_function_flattening = false,
bulwahn@35324
   109
  no_higher_order_predicate = [],
bulwahn@40054
   110
  smart_depth_limiting = true,
bulwahn@36250
   111
  no_topmost_reordering = false
bulwahn@35324
   112
}
bulwahn@35324
   113
bulwahn@35324
   114
val debug_options = Options {
bulwahn@35324
   115
  expected_modes = NONE,
bulwahn@39383
   116
  proposed_modes = [],
bulwahn@35324
   117
  proposed_names = [],
bulwahn@33257
   118
  show_steps = true,
bulwahn@33257
   119
  show_intermediate_results = true,
bulwahn@33257
   120
  show_proof_trace = false,
bulwahn@35324
   121
  show_modes = true,
bulwahn@35324
   122
  show_mode_inference = true,
bulwahn@34948
   123
  show_compilation = false,
bulwahn@35324
   124
  show_caught_failures = true,
bulwahn@39383
   125
  show_invalid_clauses = false,
bulwahn@33257
   126
  skip_proof = false,
bulwahn@34948
   127
  compilation = Random,
bulwahn@35324
   128
  inductify = true,
bulwahn@36256
   129
  specialise = true,
bulwahn@36256
   130
  detect_switches = false,
bulwahn@35324
   131
  function_flattening = true,
bulwahn@35324
   132
  fail_safe_function_flattening = false,
bulwahn@35324
   133
  no_higher_order_predicate = [],
bulwahn@40054
   134
  smart_depth_limiting = true,
bulwahn@35324
   135
  no_topmost_reordering = true
bulwahn@33257
   136
}
bulwahn@33257
   137
bulwahn@35324
   138
bulwahn@35324
   139
fun set_function_flattening b
bulwahn@35324
   140
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   141
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   142
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   143
    show_invalid_clauses = s_ic, skip_proof = s_p,
haftmann@51143
   144
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _, 
bulwahn@35324
   145
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   146
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   147
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   148
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   149
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   150
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   151
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
bulwahn@35324
   152
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
bulwahn@40054
   153
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   154
bulwahn@35324
   155
fun set_fail_safe_function_flattening b
bulwahn@35324
   156
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   157
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   158
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   159
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   160
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
haftmann@51143
   161
    fail_safe_function_flattening = _, no_higher_order_predicate = no_ho,
bulwahn@40054
   162
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   163
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   164
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   165
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   166
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   167
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
bulwahn@35324
   168
    fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
bulwahn@40054
   169
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   170
bulwahn@35324
   171
fun set_no_higher_order_predicate ss
bulwahn@35324
   172
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   173
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   174
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   175
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   176
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
haftmann@51143
   177
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = _,
bulwahn@40054
   178
    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
bulwahn@35324
   179
  (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
bulwahn@35324
   180
    show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
bulwahn@39383
   181
    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
bulwahn@39383
   182
    show_invalid_clauses = s_ic, skip_proof = s_p,
bulwahn@36256
   183
    compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
bulwahn@40054
   184
    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss,
bulwahn@40054
   185
    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
bulwahn@35324
   186
bulwahn@35324
   187
bulwahn@35324
   188
fun get_options () = 
bulwahn@35324
   189
  set_no_higher_order_predicate (!no_higher_order_predicate)
bulwahn@45450
   190
    (if !debug then debug_options else options)
bulwahn@35324
   191
bulwahn@45461
   192
val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns
bulwahn@45450
   193
val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
bulwahn@45450
   194
val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns
bulwahn@36025
   195
bulwahn@45461
   196
val mk_randompredT = Predicate_Compile_Aux.mk_monadT RandomPredCompFuns.compfuns
bulwahn@36046
   197
val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
bulwahn@36046
   198
val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
bulwahn@33250
   199
bulwahn@40054
   200
val mk_new_randompredT =
bulwahn@45461
   201
  Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40054
   202
val mk_new_return =
bulwahn@40103
   203
  Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40054
   204
val mk_new_bind =
bulwahn@40103
   205
  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   206
bulwahn@40103
   207
val mk_new_dseqT =
bulwahn@45461
   208
  Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   209
val mk_gen_return =
bulwahn@40103
   210
  Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   211
val mk_gen_bind =
bulwahn@40103
   212
  Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40103
   213
  
bulwahn@36025
   214
bulwahn@45450
   215
val mk_cpsT =
bulwahn@45461
   216
  Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns
bulwahn@45450
   217
krauss@39756
   218
val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
bulwahn@33250
   219
wenzelm@42014
   220
fun cpu_time description e =
wenzelm@42014
   221
  let val ({cpu, ...}, result) = Timing.timing e ()
wenzelm@42014
   222
  in (result, (description, Time.toMilliseconds cpu)) end
bulwahn@35324
   223
bulwahn@43886
   224
fun compile_term compilation options ctxt t =
bulwahn@35324
   225
  let
wenzelm@44241
   226
    val t' = fold_rev absfree (Term.add_frees t []) t
wenzelm@42361
   227
    val thy = Theory.copy (Proof_Context.theory_of ctxt)
bulwahn@39541
   228
    val ((((full_constname, constT), vs'), intro), thy1) =
bulwahn@42031
   229
      Predicate_Compile_Aux.define_quickcheck_predicate t' thy
bulwahn@35324
   230
    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
haftmann@51143
   231
    val (thy3, _) = cpu_time "predicate preprocessing"
bulwahn@39541
   232
        (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
haftmann@51143
   233
    val (thy4, _) = cpu_time "random_dseq core compilation"
bulwahn@36025
   234
        (fn () =>
bulwahn@36025
   235
          case compilation of
bulwahn@36025
   236
            Pos_Random_DSeq =>
bulwahn@36025
   237
              Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3
bulwahn@36025
   238
          | New_Pos_Random_DSeq =>
bulwahn@36025
   239
              Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
bulwahn@40103
   240
          | Pos_Generator_DSeq =>
bulwahn@40103
   241
              Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
bulwahn@45450
   242
          | Pos_Generator_CPS =>
bulwahn@45450
   243
               Predicate_Compile_Core.add_generator_cps_equations options [full_constname] thy3
bulwahn@36025
   244
          (*| Depth_Limited_Random =>
bulwahn@36025
   245
              Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
bulwahn@36256
   246
    (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
wenzelm@42361
   247
    val ctxt4 = Proof_Context.init_global thy4
bulwahn@40054
   248
    val modes = Core_Data.modes_of compilation ctxt4 full_constname
bulwahn@34948
   249
    val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
bulwahn@33250
   250
    val prog =
bulwahn@34948
   251
      if member eq_mode modes output_mode then
bulwahn@33250
   252
        let
bulwahn@40054
   253
          val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
bulwahn@36025
   254
          val T = 
bulwahn@36025
   255
            case compilation of
bulwahn@36025
   256
              Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@36025
   257
            | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@40103
   258
            | Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@36025
   259
            | Depth_Limited_Random =>
haftmann@51143
   260
              [@{typ natural}, @{typ natural}, @{typ natural},
haftmann@50057
   261
              @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@45450
   262
            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
bulwahn@34948
   263
        in
bulwahn@34948
   264
          Const (name, T)
bulwahn@34948
   265
        end
bulwahn@35324
   266
      else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
bulwahn@45450
   267
    fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
bulwahn@36025
   268
    val qc_term =
bulwahn@36025
   269
      case compilation of
bulwahn@36025
   270
          Pos_Random_DSeq => mk_bind (prog,
bulwahn@36025
   271
            mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
bulwahn@36025
   272
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@36025
   273
        | New_Pos_Random_DSeq => mk_new_bind (prog,
bulwahn@36025
   274
            mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
bulwahn@36025
   275
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@40103
   276
        | Pos_Generator_DSeq => mk_gen_bind (prog,
bulwahn@40103
   277
            mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
bulwahn@40103
   278
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
bulwahn@45450
   279
        | Pos_Generator_CPS => prog $
bulwahn@45750
   280
            mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
bulwahn@45750
   281
            HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
bulwahn@45750
   282
                (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
wenzelm@44241
   283
        | Depth_Limited_Random => fold_rev absdummy
haftmann@51143
   284
            [@{typ natural}, @{typ natural}, @{typ natural},
haftmann@50057
   285
             @{typ Random.seed}]
bulwahn@36025
   286
            (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
bulwahn@36025
   287
            mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
bulwahn@36025
   288
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
bulwahn@36025
   289
    val prog =
bulwahn@36025
   290
      case compilation of
bulwahn@36025
   291
        Pos_Random_DSeq =>
bulwahn@36025
   292
          let
bulwahn@36025
   293
            val compiled_term =
haftmann@39471
   294
              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
haftmann@39471
   295
                thy4 (SOME target)
haftmann@51126
   296
                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
haftmann@39471
   297
                qc_term []
bulwahn@36025
   298
          in
bulwahn@36025
   299
            (fn size => fn nrandom => fn depth =>
haftmann@51126
   300
              Option.map fst (Limited_Sequence.yield
bulwahn@36025
   301
                (compiled_term nrandom size |> Random_Engine.run) depth true))
bulwahn@36025
   302
          end
bulwahn@36025
   303
      | New_Pos_Random_DSeq =>
bulwahn@36025
   304
          let
bulwahn@36025
   305
            val compiled_term =
haftmann@39471
   306
              Code_Runtime.dynamic_value_strict
haftmann@39388
   307
                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
haftmann@39471
   308
                thy4 (SOME target)
bulwahn@36025
   309
                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
haftmann@51126
   310
                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
haftmann@39471
   311
                  qc_term []
bulwahn@36025
   312
          in
bulwahn@36025
   313
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
bulwahn@36025
   314
               (
bulwahn@36025
   315
               let
bulwahn@36025
   316
                 val seed = Random_Engine.next_seed ()
bulwahn@36025
   317
               in compiled_term nrandom size seed depth end))
bulwahn@36025
   318
          end
bulwahn@40103
   319
      | Pos_Generator_DSeq =>
bulwahn@40103
   320
          let
bulwahn@40103
   321
            val compiled_term =
bulwahn@40103
   322
              Code_Runtime.dynamic_value_strict
bulwahn@40103
   323
                (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
bulwahn@40103
   324
                thy4 (SOME target)
haftmann@51126
   325
                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
bulwahn@40103
   326
                qc_term []
bulwahn@40103
   327
          in
bulwahn@40103
   328
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
bulwahn@40103
   329
          end
bulwahn@45450
   330
      | Pos_Generator_CPS =>
bulwahn@45450
   331
          let
bulwahn@45450
   332
            val compiled_term =
bulwahn@45450
   333
              Code_Runtime.dynamic_value_strict
bulwahn@45450
   334
                (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
bulwahn@45450
   335
                thy4 (SOME target)
bulwahn@45750
   336
                (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
bulwahn@45450
   337
                qc_term []
bulwahn@45450
   338
          in
haftmann@51143
   339
            fn _ => fn _ => Option.map snd o compiled_term
bulwahn@45450
   340
          end
bulwahn@40103
   341
       | Depth_Limited_Random =>
bulwahn@36025
   342
          let
haftmann@39471
   343
            val compiled_term = Code_Runtime.dynamic_value_strict
haftmann@39388
   344
              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
haftmann@39471
   345
                thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
bulwahn@36025
   346
                  g depth nrandom size seed |> (Predicate.map o map) proc)
haftmann@39471
   347
                qc_term []
bulwahn@36025
   348
          in
bulwahn@36025
   349
            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
bulwahn@36025
   350
              (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
bulwahn@36025
   351
          end
bulwahn@33250
   352
  in
bulwahn@36025
   353
    prog
bulwahn@35324
   354
  end
bulwahn@35324
   355
bulwahn@45214
   356
fun try_upto_depth ctxt f =
bulwahn@35324
   357
  let
bulwahn@45214
   358
    val max_depth = Config.get ctxt Quickcheck.depth
bulwahn@45214
   359
    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
bulwahn@45214
   360
    fun try' i =
bulwahn@45214
   361
      if i <= max_depth then
bulwahn@35324
   362
        let
bulwahn@45214
   363
          val _ = message ("Depth: " ^ string_of_int i)
bulwahn@45214
   364
          val (result, time) =
bulwahn@45214
   365
            cpu_time ("Depth " ^ string_of_int i) (fn () =>
bulwahn@45214
   366
              f i handle Match => (if Config.get ctxt Quickcheck.quiet then ()
bulwahn@45214
   367
                    else warning "Exception Match raised during quickcheck"; NONE))
bulwahn@45214
   368
         val _ = if Config.get ctxt Quickcheck.timing then
bulwahn@45214
   369
           message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
bulwahn@35324
   370
        in
bulwahn@45214
   371
          case result of NONE => try' (i + 1) | SOME q => SOME q
bulwahn@35324
   372
        end
bulwahn@35324
   373
      else
bulwahn@35324
   374
        NONE
bulwahn@35324
   375
  in
bulwahn@35324
   376
    try' 0
bulwahn@35324
   377
  end
bulwahn@35324
   378
bulwahn@35324
   379
(* quickcheck interface functions *)
bulwahn@35324
   380
haftmann@51143
   381
fun compile_term' compilation options ctxt (t, _) =
bulwahn@35324
   382
  let
bulwahn@43886
   383
    val size = Config.get ctxt Quickcheck.size
bulwahn@36025
   384
    val c = compile_term compilation options ctxt t
haftmann@51143
   385
    val counterexample = try_upto_depth ctxt (c (Code_Numeral.natural_of_integer size)
haftmann@51143
   386
      (Code_Numeral.natural_of_integer (!nrandom)) o Code_Numeral.natural_of_integer)
bulwahn@35324
   387
  in
bulwahn@43886
   388
    Quickcheck.Result
bulwahn@45750
   389
      {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
bulwahn@43886
   390
       evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
bulwahn@35324
   391
  end
bulwahn@35324
   392
bulwahn@45214
   393
fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening =
bulwahn@35324
   394
  let
bulwahn@35324
   395
     val options =
bulwahn@35324
   396
       set_fail_safe_function_flattening fail_safe_function_flattening
bulwahn@35324
   397
         (set_function_flattening function_flattening (get_options ()))
bulwahn@35324
   398
  in
bulwahn@45214
   399
    compile_term' compilation options
bulwahn@33250
   400
  end
bulwahn@33250
   401
bulwahn@43886
   402
haftmann@51143
   403
fun test_goals options ctxt _ insts goals =
bulwahn@43886
   404
  let
bulwahn@45450
   405
    val (compilation, fail_safe_function_flattening) = options
bulwahn@45450
   406
    val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion)
bulwahn@45214
   407
    val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
bulwahn@43886
   408
    val test_term =
bulwahn@45214
   409
      quickcheck_compile_term compilation function_flattening fail_safe_function_flattening
bulwahn@43886
   410
  in
bulwahn@45214
   411
    Quickcheck_Common.collect_results (test_term ctxt)
bulwahn@43886
   412
      (maps (map snd) correct_inst_goals) []
bulwahn@43886
   413
  end
bulwahn@45450
   414
bulwahn@45450
   415
val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
bulwahn@45450
   416
val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
bulwahn@43886
   417
bulwahn@45484
   418
val setup =
bulwahn@45484
   419
  Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
bulwahn@45484
   420
  #> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
bulwahn@45450
   421
    (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
bulwahn@45450
   422
  #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
bulwahn@45450
   423
    (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
bulwahn@43886
   424
bulwahn@33250
   425
end;