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 |