--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Nov 13 09:08:32 2012 +0100
@@ -6,6 +6,7 @@
signature PREDICATE_COMPILE_CORE =
sig
+ type seed = Random_Engine.seed
type mode = Predicate_Compile_Aux.mode
type options = Predicate_Compile_Aux.options
type compilation = Predicate_Compile_Aux.compilation
@@ -23,18 +24,18 @@
val print_all_modes : compilation -> Proof.context -> unit
val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
- val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
+ val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
Proof.context -> Proof.context
val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
- val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
+ val put_dseq_random_result : (unit -> int -> int -> seed -> term DSequence.dseq * seed) ->
Proof.context -> Proof.context
val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val put_lseq_random_result :
- (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
+ (unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val put_lseq_random_stats_result :
- (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
+ (unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val code_pred_intro_attrib : attribute
@@ -70,6 +71,9 @@
open Mode_Inference;
open Predicate_Compile_Proof;
+type seed = Random_Engine.seed;
+
+
(** fundamentals **)
(* syntactic operations *)
@@ -1635,7 +1639,7 @@
structure Pred_Random_Result = Proof_Data
(
- type T = unit -> int * int -> term Predicate.pred * (int * int)
+ type T = unit -> seed -> term Predicate.pred * seed
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Pred_Random_Result"
);
@@ -1651,7 +1655,7 @@
structure Dseq_Random_Result = Proof_Data
(
- type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
+ type T = unit -> int -> int -> seed -> term DSequence.dseq * seed
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Dseq_Random_Result"
);
@@ -1667,7 +1671,7 @@
structure Lseq_Random_Result = Proof_Data
(
- type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
+ type T = unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Lseq_Random_Result"
);
@@ -1675,7 +1679,7 @@
structure Lseq_Random_Stats_Result = Proof_Data
(
- type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
+ type T = unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Lseq_Random_Stats_Result"
);
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Nov 13 09:08:32 2012 +0100
@@ -6,15 +6,16 @@
signature PREDICATE_COMPILE_QUICKCHECK =
sig
+ type seed = Random_Engine.seed
(*val quickcheck : Proof.context -> term -> int -> term list option*)
val put_pred_result :
- (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
+ (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
Proof.context -> Proof.context;
val put_dseq_result :
- (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
+ (unit -> int -> int -> seed -> term list DSequence.dseq * seed) ->
Proof.context -> Proof.context;
val put_lseq_result :
- (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
+ (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context;
val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
@@ -34,11 +35,13 @@
open Predicate_Compile_Aux;
+type seed = Random_Engine.seed:
+
(* FIXME just one data slot (record) per program unit *)
structure Pred_Result = Proof_Data
(
- type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
+ type T = unit -> int -> int -> int -> seed -> term list Predicate.pred
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Pred_Result"
);
@@ -46,7 +49,7 @@
structure Dseq_Result = Proof_Data
(
- type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
+ type T = unit -> int -> int -> seed -> term list DSequence.dseq * seed
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Dseq_Result"
);
@@ -54,7 +57,7 @@
structure Lseq_Result = Proof_Data
(
- type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
+ type T = unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Lseq_Result"
);
@@ -259,7 +262,7 @@
| Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
| Depth_Limited_Random =>
[@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
- @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
+ @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
| Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
in
Const (name, T)
@@ -283,7 +286,7 @@
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))
| Depth_Limited_Random => fold_rev absdummy
[@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
- @{typ "code_numeral * code_numeral"}]
+ @{typ Random.seed}]
(mk_bind' (list_comb (prog, map Bound (3 downto 0)),
mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))