src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
changeset 51126 df86080de4cb
parent 50093 a2886be4d615
child 51143 0a2371e7ced3
equal deleted inserted replaced
51125:f90874d3a246 51126:df86080de4cb
    10   (*val quickcheck : Proof.context -> term -> int -> term list option*)
    10   (*val quickcheck : Proof.context -> term -> int -> term list option*)
    11   val put_pred_result :
    11   val put_pred_result :
    12     (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
    12     (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
    13       Proof.context -> Proof.context;
    13       Proof.context -> Proof.context;
    14   val put_dseq_result :
    14   val put_dseq_result :
    15     (unit -> int -> int -> seed -> term list DSequence.dseq * seed) ->
    15     (unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed) ->
    16       Proof.context -> Proof.context;
    16       Proof.context -> Proof.context;
    17   val put_lseq_result :
    17   val put_lseq_result :
    18     (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
    18     (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
    19       Proof.context -> Proof.context;
    19       Proof.context -> Proof.context;
    20   val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
    20   val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
    47 );
    47 );
    48 val put_pred_result = Pred_Result.put;
    48 val put_pred_result = Pred_Result.put;
    49 
    49 
    50 structure Dseq_Result = Proof_Data
    50 structure Dseq_Result = Proof_Data
    51 (
    51 (
    52   type T = unit -> int -> int -> seed -> term list DSequence.dseq * seed
    52   type T = unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed
    53   (* FIXME avoid user error with non-user text *)
    53   (* FIXME avoid user error with non-user text *)
    54   fun init _ () = error "Dseq_Result"
    54   fun init _ () = error "Dseq_Result"
    55 );
    55 );
    56 val put_dseq_result = Dseq_Result.put;
    56 val put_dseq_result = Dseq_Result.put;
    57 
    57 
   295         Pos_Random_DSeq =>
   295         Pos_Random_DSeq =>
   296           let
   296           let
   297             val compiled_term =
   297             val compiled_term =
   298               Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
   298               Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
   299                 thy4 (SOME target)
   299                 thy4 (SOME target)
   300                 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
   300                 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
   301                 qc_term []
   301                 qc_term []
   302           in
   302           in
   303             (fn size => fn nrandom => fn depth =>
   303             (fn size => fn nrandom => fn depth =>
   304               Option.map fst (DSequence.yield
   304               Option.map fst (Limited_Sequence.yield
   305                 (compiled_term nrandom size |> Random_Engine.run) depth true))
   305                 (compiled_term nrandom size |> Random_Engine.run) depth true))
   306           end
   306           end
   307       | New_Pos_Random_DSeq =>
   307       | New_Pos_Random_DSeq =>
   308           let
   308           let
   309             val compiled_term =
   309             val compiled_term =
   310               Code_Runtime.dynamic_value_strict
   310               Code_Runtime.dynamic_value_strict
   311                 (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
   311                 (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
   312                 thy4 (SOME target)
   312                 thy4 (SOME target)
   313                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
   313                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
   314                   g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
   314                   g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
   315                   qc_term []
   315                   qc_term []
   316           in
   316           in
   317             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
   317             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
   318                (
   318                (
   319                let
   319                let
   324           let
   324           let
   325             val compiled_term =
   325             val compiled_term =
   326               Code_Runtime.dynamic_value_strict
   326               Code_Runtime.dynamic_value_strict
   327                 (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
   327                 (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
   328                 thy4 (SOME target)
   328                 thy4 (SOME target)
   329                 (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.mapa o map) proc)
   329                 (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
   330                 qc_term []
   330                 qc_term []
   331           in
   331           in
   332             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
   332             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
   333           end
   333           end
   334       | Pos_Generator_CPS =>
   334       | Pos_Generator_CPS =>