1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 13 09:08:32 2012 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature PREDICATE_COMPILE_CORE =
     1.6  sig
     1.7 +  type seed = Random_Engine.seed
     1.8    type mode = Predicate_Compile_Aux.mode
     1.9    type options = Predicate_Compile_Aux.options
    1.10    type compilation = Predicate_Compile_Aux.compilation
    1.11 @@ -23,18 +24,18 @@
    1.12    val print_all_modes : compilation -> Proof.context -> unit
    1.13  
    1.14    val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
    1.15 -  val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
    1.16 +  val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
    1.17      Proof.context -> Proof.context
    1.18    val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
    1.19 -  val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
    1.20 +  val put_dseq_random_result : (unit -> int -> int -> seed -> term DSequence.dseq * seed) ->
    1.21      Proof.context -> Proof.context
    1.22    val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
    1.23      Proof.context -> Proof.context
    1.24    val put_lseq_random_result :
    1.25 -    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
    1.26 +    (unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence) ->
    1.27      Proof.context -> Proof.context
    1.28    val put_lseq_random_stats_result :
    1.29 -    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
    1.30 +    (unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
    1.31      Proof.context -> Proof.context
    1.32  
    1.33    val code_pred_intro_attrib : attribute
    1.34 @@ -70,6 +71,9 @@
    1.35  open Mode_Inference;
    1.36  open Predicate_Compile_Proof;
    1.37  
    1.38 +type seed = Random_Engine.seed;
    1.39 +
    1.40 +
    1.41  (** fundamentals **)
    1.42  
    1.43  (* syntactic operations *)
    1.44 @@ -1635,7 +1639,7 @@
    1.45  
    1.46  structure Pred_Random_Result = Proof_Data
    1.47  (
    1.48 -  type T = unit -> int * int -> term Predicate.pred * (int * int)
    1.49 +  type T = unit -> seed -> term Predicate.pred * seed
    1.50    (* FIXME avoid user error with non-user text *)
    1.51    fun init _ () = error "Pred_Random_Result"
    1.52  );
    1.53 @@ -1651,7 +1655,7 @@
    1.54  
    1.55  structure Dseq_Random_Result = Proof_Data
    1.56  (
    1.57 -  type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
    1.58 +  type T = unit -> int -> int -> seed -> term DSequence.dseq * seed
    1.59    (* FIXME avoid user error with non-user text *)
    1.60    fun init _ () = error "Dseq_Random_Result"
    1.61  );
    1.62 @@ -1667,7 +1671,7 @@
    1.63  
    1.64  structure Lseq_Random_Result = Proof_Data
    1.65  (
    1.66 -  type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
    1.67 +  type T = unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence
    1.68    (* FIXME avoid user error with non-user text *)
    1.69    fun init _ () = error "Lseq_Random_Result"
    1.70  );
    1.71 @@ -1675,7 +1679,7 @@
    1.72  
    1.73  structure Lseq_Random_Stats_Result = Proof_Data
    1.74  (
    1.75 -  type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
    1.76 +  type T = unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence
    1.77    (* FIXME avoid user error with non-user text *)
    1.78    fun init _ () = error "Lseq_Random_Stats_Result"
    1.79  );

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Nov 12 23:24:40 2012 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Nov 13 09:08:32 2012 +0100
     2.3 @@ -6,15 +6,16 @@
     2.4  
     2.5  signature PREDICATE_COMPILE_QUICKCHECK =
     2.6  sig
     2.7 +  type seed = Random_Engine.seed
     2.8    (*val quickcheck : Proof.context -> term -> int -> term list option*)
     2.9    val put_pred_result :
    2.10 -    (unit -> int -> int -> int -> int * int -> term list Predicate.pred) ->
    2.11 +    (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
    2.12        Proof.context -> Proof.context;
    2.13    val put_dseq_result :
    2.14 -    (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) ->
    2.15 +    (unit -> int -> int -> seed -> term list DSequence.dseq * seed) ->
    2.16        Proof.context -> Proof.context;
    2.17    val put_lseq_result :
    2.18 -    (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) ->
    2.19 +    (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
    2.20        Proof.context -> Proof.context;
    2.21    val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
    2.22      Proof.context -> Proof.context
    2.23 @@ -34,11 +35,13 @@
    2.24  
    2.25  open Predicate_Compile_Aux;
    2.26  
    2.27 +type seed = Random_Engine.seed:
    2.28 +
    2.29  (* FIXME just one data slot (record) per program unit *)
    2.30  
    2.31  structure Pred_Result = Proof_Data
    2.32  (
    2.33 -  type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
    2.34 +  type T = unit -> int -> int -> int -> seed -> term list Predicate.pred
    2.35    (* FIXME avoid user error with non-user text *)
    2.36    fun init _ () = error "Pred_Result"
    2.37  );
    2.38 @@ -46,7 +49,7 @@
    2.39  
    2.40  structure Dseq_Result = Proof_Data
    2.41  (
    2.42 -  type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
    2.43 +  type T = unit -> int -> int -> seed -> term list DSequence.dseq * seed
    2.44    (* FIXME avoid user error with non-user text *)
    2.45    fun init _ () = error "Dseq_Result"
    2.46  );
    2.47 @@ -54,7 +57,7 @@
    2.48  
    2.49  structure Lseq_Result = Proof_Data
    2.50  (
    2.51 -  type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
    2.52 +  type T = unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence
    2.53    (* FIXME avoid user error with non-user text *)
    2.54    fun init _ () = error "Lseq_Result"
    2.55  );
    2.56 @@ -259,7 +262,7 @@
    2.57              | Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
    2.58              | Depth_Limited_Random =>
    2.59                [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    2.60 -              @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
    2.61 +              @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
    2.62              | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
    2.63          in
    2.64            Const (name, T)
    2.65 @@ -283,7 +286,7 @@
    2.66                  (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
    2.67          | Depth_Limited_Random => fold_rev absdummy
    2.68              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    2.69 -             @{typ "code_numeral * code_numeral"}]
    2.70 +             @{typ Random.seed}]
    2.71              (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
    2.72              mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
    2.73              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))