3275 Pos_Random_DSeq => |
3275 Pos_Random_DSeq => |
3276 let |
3276 let |
3277 val [nrandom, size, depth] = arguments |
3277 val [nrandom, size, depth] = arguments |
3278 in |
3278 in |
3279 rpair NONE (fst (DSequence.yieldn k |
3279 rpair NONE (fst (DSequence.yieldn k |
3280 (Code_Eval.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result") |
3280 (Code_Runtime.eval NONE (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result") |
3281 (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc) |
3281 (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc) |
3282 thy t' [] nrandom size |
3282 thy t' [] nrandom size |
3283 |> Random_Engine.run) |
3283 |> Random_Engine.run) |
3284 depth true)) |
3284 depth true)) |
3285 end |
3285 end |
3286 | DSeq => |
3286 | DSeq => |
3287 rpair NONE (fst (DSequence.yieldn k |
3287 rpair NONE (fst (DSequence.yieldn k |
3288 (Code_Eval.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result") |
3288 (Code_Runtime.eval NONE (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result") |
3289 DSequence.map thy t' []) (the_single arguments) true)) |
3289 DSequence.map thy t' []) (the_single arguments) true)) |
3290 | New_Pos_Random_DSeq => |
3290 | New_Pos_Random_DSeq => |
3291 let |
3291 let |
3292 val [nrandom, size, depth] = arguments |
3292 val [nrandom, size, depth] = arguments |
3293 val seed = Random_Engine.next_seed () |
3293 val seed = Random_Engine.next_seed () |
3294 in |
3294 in |
3295 if stats then |
3295 if stats then |
3296 apsnd (SOME o accumulate) (split_list |
3296 apsnd (SOME o accumulate) (split_list |
3297 (fst (Lazy_Sequence.yieldn k |
3297 (fst (Lazy_Sequence.yieldn k |
3298 (Code_Eval.eval NONE |
3298 (Code_Runtime.eval NONE |
3299 (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result") |
3299 (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result") |
3300 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth |
3300 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth |
3301 |> Lazy_Sequence.mapa (apfst proc)) |
3301 |> Lazy_Sequence.mapa (apfst proc)) |
3302 thy t' [] nrandom size seed depth)))) |
3302 thy t' [] nrandom size seed depth)))) |
3303 else rpair NONE |
3303 else rpair NONE |
3304 (fst (Lazy_Sequence.yieldn k |
3304 (fst (Lazy_Sequence.yieldn k |
3305 (Code_Eval.eval NONE |
3305 (Code_Runtime.eval NONE |
3306 (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result") |
3306 (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result") |
3307 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth |
3307 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth |
3308 |> Lazy_Sequence.mapa proc) |
3308 |> Lazy_Sequence.mapa proc) |
3309 thy t' [] nrandom size seed depth))) |
3309 thy t' [] nrandom size seed depth))) |
3310 end |
3310 end |
3311 | _ => |
3311 | _ => |
3312 rpair NONE (fst (Predicate.yieldn k |
3312 rpair NONE (fst (Predicate.yieldn k |
3313 (Code_Eval.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result") |
3313 (Code_Runtime.eval NONE (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result") |
3314 Predicate.map thy t' []))) |
3314 Predicate.map thy t' []))) |
3315 in ((T, ts), statistics) end; |
3315 in ((T, ts), statistics) end; |
3316 |
3316 |
3317 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr = |
3317 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr = |
3318 let |
3318 let |