a new simpler random compilation for the predicate compiler
authorbulwahn
Mon Mar 22 08:30:13 2010 +0100 (2010-03-22)
changeset 358802623b23e41fc
parent 35879 99818df5b8f5
child 35881 aa412e08bfee
a new simpler random compilation for the predicate compiler
src/HOL/Quickcheck.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Quickcheck.thy	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -145,6 +145,23 @@
     1.4  
     1.5  subsection {* The Random-Predicate Monad *} 
     1.6  
     1.7 +fun iter' ::
     1.8 +  "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
     1.9 +where
    1.10 +  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    1.11 +     let ((x, _), seed') = random sz seed
    1.12 +   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
    1.13 +
    1.14 +definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
    1.15 +where
    1.16 +  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
    1.17 +
    1.18 +lemma [code]:
    1.19 +  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
    1.20 +     let ((x, _), seed') = random sz seed
    1.21 +   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
    1.22 +unfolding iter_def iter'.simps[of _ nrandom] ..
    1.23 +
    1.24  types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
    1.25  
    1.26  definition empty :: "'a randompred"
    1.27 @@ -182,9 +199,9 @@
    1.28  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
    1.29    where "map f P = bind P (single o f)"
    1.30  
    1.31 -hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
    1.32 +hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
    1.33  hide (open) type randompred
    1.34  hide (open) const random collapse beyond random_fun_aux random_fun_lift
    1.35 -  empty single bind union if_randompred not_randompred Random map
    1.36 +  iter' iter empty single bind union if_randompred not_randompred Random map
    1.37  
    1.38  end
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
     2.3 @@ -570,7 +570,7 @@
     2.4    "no_topmost_reordering"]
     2.5  
     2.6  val compilation_names = [("pred", Pred),
     2.7 -  (*("random", Random),*)
     2.8 +  ("random", Random),
     2.9    ("depth_limited", Depth_Limited), (*("annotated", Annotated),*)
    2.10    ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
    2.11  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     3.3 @@ -868,19 +868,6 @@
     3.4  
     3.5  end;
     3.6  
     3.7 -
     3.8 -
     3.9 -fun mk_random T =
    3.10 -  let
    3.11 -    val random = Const ("Quickcheck.random_class.random",
    3.12 -      @{typ code_numeral} --> @{typ Random.seed} -->
    3.13 -        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
    3.14 -  in
    3.15 -    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
    3.16 -      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
    3.17 -      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
    3.18 -  end;
    3.19 -
    3.20  (* for external use with interactive mode *)
    3.21  val pred_compfuns = PredicateCompFuns.compfuns
    3.22  val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
    3.23 @@ -1447,6 +1434,7 @@
    3.24    compilation : compilation,
    3.25    function_name_prefix : string,
    3.26    compfuns : compilation_funs,
    3.27 +  mk_random : typ -> term list -> term,
    3.28    modify_funT : typ -> typ,
    3.29    additional_arguments : string list -> term list,
    3.30    wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
    3.31 @@ -1459,6 +1447,7 @@
    3.32  val function_name_prefix = #function_name_prefix o dest_comp_modifiers
    3.33  val compfuns = #compfuns o dest_comp_modifiers
    3.34  
    3.35 +val mk_random = #mk_random o dest_comp_modifiers
    3.36  val funT_of' = funT_of o compfuns
    3.37  val modify_funT = #modify_funT o dest_comp_modifiers
    3.38  fun funT_of comp mode = modify_funT comp o funT_of' comp mode
    3.39 @@ -1612,8 +1601,7 @@
    3.40                   end
    3.41               | Generator (v, T) =>
    3.42                   let
    3.43 -                   val u = mk_random T
    3.44 -                   
    3.45 +                   val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
    3.46                     val rest = compile_prems [Free (v, T)]  vs' names'' ps;
    3.47                   in
    3.48                     (u, rest)
    3.49 @@ -2543,9 +2531,10 @@
    3.50    compilation = Depth_Limited,
    3.51    function_name_prefix = "depth_limited_",
    3.52    compfuns = PredicateCompFuns.compfuns,
    3.53 +  mk_random = (fn _ => error "no random generation"),
    3.54    additional_arguments = fn names =>
    3.55      let
    3.56 -      val [depth_name] = Name.variant_list names ["depth"]
    3.57 +      val depth_name = Name.variant names "depth"
    3.58      in [Free (depth_name, @{typ code_numeral})] end,
    3.59    modify_funT = (fn T => let val (Ts, U) = strip_type T
    3.60    val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
    3.61 @@ -2570,20 +2559,33 @@
    3.62            $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
    3.63      in [depth'] end
    3.64    }
    3.65 -(*
    3.66 +
    3.67  val random_comp_modifiers = Comp_Mod.Comp_Modifiers
    3.68    {
    3.69    compilation = Random,
    3.70 -  function_name_of = function_name_of Random,
    3.71 -  set_function_name = set_function_name Random,
    3.72    function_name_prefix = "random_",
    3.73 -  funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
    3.74 -  additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
    3.75 +  compfuns = PredicateCompFuns.compfuns,
    3.76 +  mk_random = (fn T => fn additional_arguments =>
    3.77 +  list_comb (Const(@{const_name Quickcheck.iter},
    3.78 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    3.79 +    PredicateCompFuns.mk_predT T), additional_arguments)),
    3.80 +  modify_funT = (fn T =>
    3.81 +    let
    3.82 +      val (Ts, U) = strip_type T
    3.83 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
    3.84 +    in (Ts @ Ts') ---> U end),
    3.85 +  additional_arguments = (fn names =>
    3.86 +    let
    3.87 +      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
    3.88 +    in
    3.89 +      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
    3.90 +        Free (seed, @{typ "code_numeral * code_numeral"})]
    3.91 +    end),
    3.92    wrap_compilation = K (K (K (K (K I))))
    3.93      : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    3.94    transform_additional_arguments = K I : (indprem -> term list -> term list)
    3.95    }
    3.96 -*)
    3.97 +
    3.98  (* different instantiantions of the predicate compiler *)
    3.99  
   3.100  val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
   3.101 @@ -2591,7 +2593,8 @@
   3.102    compilation = Pred,
   3.103    function_name_prefix = "",
   3.104    compfuns = PredicateCompFuns.compfuns,
   3.105 -    modify_funT = I,
   3.106 +  mk_random = (fn _ => error "no random generation"),
   3.107 +  modify_funT = I,
   3.108    additional_arguments = K [],
   3.109    wrap_compilation = K (K (K (K (K I))))
   3.110     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   3.111 @@ -2615,6 +2618,7 @@
   3.112    compilation = Annotated,
   3.113    function_name_prefix = "annotated_",
   3.114    compfuns = PredicateCompFuns.compfuns,
   3.115 +  mk_random = (fn _ => error "no random generation"),
   3.116    modify_funT = I,
   3.117    additional_arguments = K [],
   3.118    wrap_compilation =
   3.119 @@ -2629,6 +2633,7 @@
   3.120    compilation = DSeq,
   3.121    function_name_prefix = "dseq_",
   3.122    compfuns = DSequence_CompFuns.compfuns,
   3.123 +  mk_random = (fn _ => error "no random generation"),
   3.124    modify_funT = I,
   3.125    additional_arguments = K [],
   3.126    wrap_compilation = K (K (K (K (K I))))
   3.127 @@ -2641,6 +2646,17 @@
   3.128    compilation = Pos_Random_DSeq,
   3.129    function_name_prefix = "random_dseq_",
   3.130    compfuns = Random_Sequence_CompFuns.compfuns,
   3.131 +  mk_random = (fn T => fn additional_arguments =>
   3.132 +  let
   3.133 +    val random = Const ("Quickcheck.random_class.random",
   3.134 +      @{typ code_numeral} --> @{typ Random.seed} -->
   3.135 +        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   3.136 +  in
   3.137 +    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   3.138 +      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   3.139 +      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   3.140 +  end),
   3.141 +
   3.142    modify_funT = I,
   3.143    additional_arguments = K [],
   3.144    wrap_compilation = K (K (K (K (K I))))
   3.145 @@ -2653,6 +2669,7 @@
   3.146    compilation = Neg_Random_DSeq,
   3.147    function_name_prefix = "random_dseq_neg_",
   3.148    compfuns = Random_Sequence_CompFuns.compfuns,
   3.149 +  mk_random = (fn _ => error "no random generation"),
   3.150    modify_funT = I,
   3.151    additional_arguments = K [],
   3.152    wrap_compilation = K (K (K (K (K I))))
   3.153 @@ -2683,16 +2700,19 @@
   3.154    comp_modifiers = annotated_comp_modifiers,
   3.155    use_random = false,
   3.156    qname = "annotated_equation"})
   3.157 -(*
   3.158 -val add_quickcheck_equations = gen_add_equations
   3.159 -  (Steps {infer_modes = infer_modes_with_generator,
   3.160 -  define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
   3.161 -  compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
   3.162 +
   3.163 +val add_random_equations = gen_add_equations
   3.164 +  (Steps {
   3.165 +  define_functions =
   3.166 +    fn options => fn preds => fn (s, modes) =>
   3.167 +      define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
   3.168 +      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   3.169 +  comp_modifiers = random_comp_modifiers,
   3.170    prove = prove_by_skip,
   3.171    add_code_equations = K (K I),
   3.172 -  defined = defined_functions Random,
   3.173 +  use_random = true,
   3.174    qname = "random_equation"})
   3.175 -*)
   3.176 +
   3.177  val add_dseq_equations = gen_add_equations
   3.178    (Steps {
   3.179    define_functions =
   3.180 @@ -2777,9 +2797,8 @@
   3.181             | DSeq => add_dseq_equations
   3.182             | Pos_Random_DSeq => add_random_dseq_equations
   3.183             | Depth_Limited => add_depth_limited_equations
   3.184 +           | Random => add_random_equations
   3.185             | compilation => error ("Compilation not supported")
   3.186 -           (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs)
   3.187 -           | Annotated => add_annotated_equations*)
   3.188             ) options [const]))
   3.189        end
   3.190    in
   3.191 @@ -2858,7 +2877,8 @@
   3.192          val additional_arguments =
   3.193            case compilation of
   3.194              Pred => []
   3.195 -          | Random => [@{term "5 :: code_numeral"}]
   3.196 +          | Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
   3.197 +            [@{term "(1, 1) :: code_numeral * code_numeral"}]
   3.198            | Annotated => []
   3.199            | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
   3.200            | DSeq => []
   3.201 @@ -2885,7 +2905,7 @@
   3.202    let
   3.203      val compfuns =
   3.204        case compilation of
   3.205 -        Random => RandomPredCompFuns.compfuns
   3.206 +        Random => PredicateCompFuns.compfuns
   3.207        | DSeq => DSequence_CompFuns.compfuns
   3.208        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
   3.209        | _ => PredicateCompFuns.compfuns
   3.210 @@ -2894,12 +2914,12 @@
   3.211      val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
   3.212      val ts =
   3.213        case compilation of
   3.214 -        Random =>
   3.215 +       (* Random =>
   3.216            fst (Predicate.yieldn k
   3.217            (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
   3.218              (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
   3.219 -            |> Random_Engine.run))
   3.220 -      | Pos_Random_DSeq =>
   3.221 +            |> Random_Engine.run))*)
   3.222 +        Pos_Random_DSeq =>
   3.223            let
   3.224              val [nrandom, size, depth] = arguments
   3.225            in