adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
authorbulwahn
Mon Mar 29 17:30:38 2010 +0200 (2010-03-29)
changeset 360203ee4c29ead7f
parent 36019 64bbbd858c39
child 36021 c86fcf44b4c9
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
src/HOL/Lazy_Sequence.thy
src/HOL/Random.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:36 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:38 2010 +0200
     1.3 @@ -131,6 +131,7 @@
     1.4    datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
     1.5    val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
     1.6    val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
     1.7 +  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
     1.8  end;
     1.9  
    1.10  structure Lazy_Sequence : LAZY_SEQUENCE =
    1.11 @@ -142,6 +143,8 @@
    1.12  
    1.13  val yieldn = @{code yieldn}
    1.14  
    1.15 +val map = @{code map}
    1.16 +
    1.17  end;
    1.18  *}
    1.19  
     2.1 --- a/src/HOL/Random.thy	Mon Mar 29 17:30:36 2010 +0200
     2.2 +++ b/src/HOL/Random.thy	Mon Mar 29 17:30:38 2010 +0200
     2.3 @@ -1,3 +1,4 @@
     2.4 +
     2.5  (* Author: Florian Haftmann, TU Muenchen *)
     2.6  
     2.7  header {* A HOL random engine *}
     2.8 @@ -154,6 +155,14 @@
     2.9  
    2.10  in
    2.11  
    2.12 +fun next_seed () =
    2.13 +  let
    2.14 +    val (seed1, seed') = @{code split_seed} (! seed)
    2.15 +    val _ = seed := seed'
    2.16 +  in
    2.17 +    seed1
    2.18 +  end
    2.19 +
    2.20  fun run f =
    2.21    let
    2.22      val (x, seed') = f (! seed);
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:36 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:38 2010 +0200
     3.3 @@ -39,6 +39,9 @@
     3.4    val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
     3.5    val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
     3.6      option Unsynchronized.ref
     3.7 +  val new_random_dseq_eval_ref :
     3.8 +    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
     3.9 +      option Unsynchronized.ref
    3.10    val code_pred_intro_attrib : attribute
    3.11    
    3.12    (* used by Quickcheck_Generator *) 
    3.13 @@ -58,8 +61,10 @@
    3.14    
    3.15    val pred_compfuns : compilation_funs
    3.16    val randompred_compfuns : compilation_funs
    3.17 +  val new_randompred_compfuns : compilation_funs
    3.18    val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    3.19    val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    3.20 +  val add_new_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    3.21    val mk_tracing : string -> term -> term
    3.22  end;
    3.23  
    3.24 @@ -1020,6 +1025,7 @@
    3.25  (* for external use with interactive mode *)
    3.26  val pred_compfuns = PredicateCompFuns.compfuns
    3.27  val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
    3.28 +val new_randompred_compfuns = New_Pos_Random_Sequence_CompFuns.compfuns
    3.29  
    3.30  (* compilation modifiers *)
    3.31  
    3.32 @@ -1892,7 +1898,7 @@
    3.33    | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
    3.34    | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
    3.35  
    3.36 -fun compile_expr compilation_modifiers ctxt pol (t, deriv) additional_arguments =
    3.37 +fun compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments =
    3.38    let
    3.39      val compfuns = Comp_Mod.compfuns compilation_modifiers
    3.40      fun expr_of (t, deriv) =
    3.41 @@ -1926,7 +1932,7 @@
    3.42    end
    3.43  
    3.44  fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
    3.45 -  (pol, mode) inp (ts, moded_ps) =
    3.46 +  mode inp (ts, moded_ps) =
    3.47    let
    3.48      val compfuns = Comp_Mod.compfuns compilation_modifiers
    3.49      val iss = ho_arg_modes_of mode
    3.50 @@ -1959,8 +1965,7 @@
    3.51                 Prem t =>
    3.52                   let
    3.53                     val u =
    3.54 -                     compile_expr compilation_modifiers ctxt
    3.55 -                       pol (t, deriv) additional_arguments'
    3.56 +                     compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments'
    3.57                     val (_, out_ts''') = split_mode mode (snd (strip_comb t))
    3.58                     val rest = compile_prems out_ts''' vs' names'' ps
    3.59                   in
    3.60 @@ -1971,8 +1976,7 @@
    3.61                     val neg_compilation_modifiers =
    3.62                       negative_comp_modifiers_of compilation_modifiers
    3.63                     val u = mk_not compfuns
    3.64 -                     (compile_expr neg_compilation_modifiers ctxt
    3.65 -                       (not pol) (t, deriv) additional_arguments')
    3.66 +                     (compile_expr neg_compilation_modifiers ctxt (t, deriv) additional_arguments')
    3.67                     val (_, out_ts''') = split_mode mode (snd (strip_comb t))
    3.68                     val rest = compile_prems out_ts''' vs' names'' ps
    3.69                   in
    3.70 @@ -2005,6 +2009,8 @@
    3.71  fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
    3.72    let
    3.73      val ctxt = ProofContext.init thy
    3.74 +    val compilation_modifiers = if pol then compilation_modifiers else
    3.75 +      negative_comp_modifiers_of compilation_modifiers
    3.76      val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
    3.77        (all_vs @ param_vs)
    3.78      val compfuns = Comp_Mod.compfuns compilation_modifiers
    3.79 @@ -2029,7 +2035,7 @@
    3.80        (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
    3.81      val cl_ts =
    3.82        map (compile_clause compilation_modifiers
    3.83 -        ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
    3.84 +        ctxt all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls;
    3.85      val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
    3.86        s T mode additional_arguments
    3.87        (if null cl_ts then
    3.88 @@ -3127,6 +3133,8 @@
    3.89  val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
    3.90  val random_dseq_eval_ref =
    3.91    Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
    3.92 +val new_random_dseq_eval_ref =
    3.93 +  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
    3.94  
    3.95  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
    3.96  fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
    3.97 @@ -3196,6 +3204,7 @@
    3.98              [@{term "(1, 1) :: code_numeral * code_numeral"}]
    3.99            | DSeq => []
   3.100            | Pos_Random_DSeq => []
   3.101 +          | New_Pos_Random_DSeq => []
   3.102          val comp_modifiers =
   3.103            case compilation of
   3.104              Pred => predicate_comp_modifiers
   3.105 @@ -3205,8 +3214,9 @@
   3.106            (*| Annotated => annotated_comp_modifiers*)
   3.107            | DSeq => dseq_comp_modifiers
   3.108            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
   3.109 +          | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
   3.110          val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
   3.111 -          true (body, deriv) additional_arguments;
   3.112 +          (body, deriv) additional_arguments;
   3.113          val T_pred = dest_predT compfuns (fastype_of t_pred)
   3.114          val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
   3.115        in
   3.116 @@ -3223,7 +3233,9 @@
   3.117          Random => PredicateCompFuns.compfuns
   3.118        | DSeq => DSequence_CompFuns.compfuns
   3.119        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
   3.120 +      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
   3.121        | _ => PredicateCompFuns.compfuns
   3.122 +      
   3.123      val t = analyze_compr thy compfuns param_user_modes options t_compr;
   3.124      val T = dest_predT compfuns (fastype_of t);
   3.125      val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
   3.126 @@ -3249,6 +3261,18 @@
   3.127            fst (DSequence.yieldn k
   3.128              (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
   3.129                DSequence.map thy t' []) (the_single arguments) true)
   3.130 +      | New_Pos_Random_DSeq =>
   3.131 +          let
   3.132 +            val [nrandom, size, depth] = arguments
   3.133 +            val seed = Random_Engine.next_seed ()
   3.134 +          in
   3.135 +            fst (Lazy_Sequence.yieldn k
   3.136 +              (Code_Eval.eval NONE
   3.137 +                ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
   3.138 +                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   3.139 +                  |> Lazy_Sequence.map proc)
   3.140 +                  thy t' [] nrandom size seed depth))
   3.141 +          end
   3.142        | _ =>
   3.143            fst (Predicate.yieldn k
   3.144              (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)