src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
changeset 59151 a012574b78e7
parent 58843 521cea5fa777
child 59154 68ca25931dce
equal deleted inserted replaced
59150:71b416020f42 59151:a012574b78e7
    42 
    42 
    43 (* FIXME just one data slot (record) per program unit *)
    43 (* FIXME just one data slot (record) per program unit *)
    44 
    44 
    45 structure Pred_Result = Proof_Data
    45 structure Pred_Result = Proof_Data
    46 (
    46 (
    47   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
    47   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    48   (* FIXME avoid user error with non-user text *)
    48     Code_Numeral.natural -> seed -> term list Predicate.pred
    49   fun init _ () = error "Pred_Result"
    49   fun init _ () = raise Fail "Pred_Result"
    50 )
    50 )
    51 val put_pred_result = Pred_Result.put
    51 val put_pred_result = Pred_Result.put
    52 
    52 
    53 structure Dseq_Result = Proof_Data
    53 structure Dseq_Result = Proof_Data
    54 (
    54 (
    55   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
    55   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    56   (* FIXME avoid user error with non-user text *)
    56     seed -> term list Limited_Sequence.dseq * seed
    57   fun init _ () = error "Dseq_Result"
    57   fun init _ () = raise Fail "Dseq_Result"
    58 )
    58 )
    59 val put_dseq_result = Dseq_Result.put
    59 val put_dseq_result = Dseq_Result.put
    60 
    60 
    61 structure Lseq_Result = Proof_Data
    61 structure Lseq_Result = Proof_Data
    62 (
    62 (
    63   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    63   type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
    64   (* FIXME avoid user error with non-user text *)
    64     seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    65   fun init _ () = error "Lseq_Result"
    65   fun init _ () = raise Fail "Lseq_Result"
    66 )
    66 )
    67 val put_lseq_result = Lseq_Result.put
    67 val put_lseq_result = Lseq_Result.put
    68 
    68 
    69 structure New_Dseq_Result = Proof_Data
    69 structure New_Dseq_Result = Proof_Data
    70 (
    70 (
    71   type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    71   type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
    72   (* FIXME avoid user error with non-user text *)
    72   fun init _ () = raise Fail "New_Dseq_Random_Result"
    73   fun init _ () = error "New_Dseq_Random_Result"
       
    74 )
    73 )
    75 val put_new_dseq_result = New_Dseq_Result.put
    74 val put_new_dseq_result = New_Dseq_Result.put
    76 
    75 
    77 structure CPS_Result = Proof_Data
    76 structure CPS_Result = Proof_Data
    78 (
    77 (
    79   type T = unit -> Code_Numeral.natural -> (bool * term list) option
    78   type T = unit -> Code_Numeral.natural -> (bool * term list) option
    80   (* FIXME avoid user error with non-user text *)
    79   fun init _ () = raise Fail "CPS_Result"
    81   fun init _ () = error "CPS_Result"
       
    82 )
    80 )
    83 val put_cps_result = CPS_Result.put
    81 val put_cps_result = CPS_Result.put
    84 
    82 
    85 val target = "Quickcheck"
    83 val target = "Quickcheck"
    86 
    84