src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 35880 2623b23e41fc
parent 35879 99818df5b8f5
child 35881 aa412e08bfee
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -868,19 +868,6 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -
     1.8 -
     1.9 -fun mk_random T =
    1.10 -  let
    1.11 -    val random = Const ("Quickcheck.random_class.random",
    1.12 -      @{typ code_numeral} --> @{typ Random.seed} -->
    1.13 -        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
    1.14 -  in
    1.15 -    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
    1.16 -      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
    1.17 -      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
    1.18 -  end;
    1.19 -
    1.20  (* for external use with interactive mode *)
    1.21  val pred_compfuns = PredicateCompFuns.compfuns
    1.22  val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
    1.23 @@ -1447,6 +1434,7 @@
    1.24    compilation : compilation,
    1.25    function_name_prefix : string,
    1.26    compfuns : compilation_funs,
    1.27 +  mk_random : typ -> term list -> term,
    1.28    modify_funT : typ -> typ,
    1.29    additional_arguments : string list -> term list,
    1.30    wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
    1.31 @@ -1459,6 +1447,7 @@
    1.32  val function_name_prefix = #function_name_prefix o dest_comp_modifiers
    1.33  val compfuns = #compfuns o dest_comp_modifiers
    1.34  
    1.35 +val mk_random = #mk_random o dest_comp_modifiers
    1.36  val funT_of' = funT_of o compfuns
    1.37  val modify_funT = #modify_funT o dest_comp_modifiers
    1.38  fun funT_of comp mode = modify_funT comp o funT_of' comp mode
    1.39 @@ -1612,8 +1601,7 @@
    1.40                   end
    1.41               | Generator (v, T) =>
    1.42                   let
    1.43 -                   val u = mk_random T
    1.44 -                   
    1.45 +                   val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
    1.46                     val rest = compile_prems [Free (v, T)]  vs' names'' ps;
    1.47                   in
    1.48                     (u, rest)
    1.49 @@ -2543,9 +2531,10 @@
    1.50    compilation = Depth_Limited,
    1.51    function_name_prefix = "depth_limited_",
    1.52    compfuns = PredicateCompFuns.compfuns,
    1.53 +  mk_random = (fn _ => error "no random generation"),
    1.54    additional_arguments = fn names =>
    1.55      let
    1.56 -      val [depth_name] = Name.variant_list names ["depth"]
    1.57 +      val depth_name = Name.variant names "depth"
    1.58      in [Free (depth_name, @{typ code_numeral})] end,
    1.59    modify_funT = (fn T => let val (Ts, U) = strip_type T
    1.60    val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
    1.61 @@ -2570,20 +2559,33 @@
    1.62            $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
    1.63      in [depth'] end
    1.64    }
    1.65 -(*
    1.66 +
    1.67  val random_comp_modifiers = Comp_Mod.Comp_Modifiers
    1.68    {
    1.69    compilation = Random,
    1.70 -  function_name_of = function_name_of Random,
    1.71 -  set_function_name = set_function_name Random,
    1.72    function_name_prefix = "random_",
    1.73 -  funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
    1.74 -  additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
    1.75 +  compfuns = PredicateCompFuns.compfuns,
    1.76 +  mk_random = (fn T => fn additional_arguments =>
    1.77 +  list_comb (Const(@{const_name Quickcheck.iter},
    1.78 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    1.79 +    PredicateCompFuns.mk_predT T), additional_arguments)),
    1.80 +  modify_funT = (fn T =>
    1.81 +    let
    1.82 +      val (Ts, U) = strip_type T
    1.83 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
    1.84 +    in (Ts @ Ts') ---> U end),
    1.85 +  additional_arguments = (fn names =>
    1.86 +    let
    1.87 +      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
    1.88 +    in
    1.89 +      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
    1.90 +        Free (seed, @{typ "code_numeral * code_numeral"})]
    1.91 +    end),
    1.92    wrap_compilation = K (K (K (K (K I))))
    1.93      : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    1.94    transform_additional_arguments = K I : (indprem -> term list -> term list)
    1.95    }
    1.96 -*)
    1.97 +
    1.98  (* different instantiantions of the predicate compiler *)
    1.99  
   1.100  val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.101 @@ -2591,7 +2593,8 @@
   1.102    compilation = Pred,
   1.103    function_name_prefix = "",
   1.104    compfuns = PredicateCompFuns.compfuns,
   1.105 -    modify_funT = I,
   1.106 +  mk_random = (fn _ => error "no random generation"),
   1.107 +  modify_funT = I,
   1.108    additional_arguments = K [],
   1.109    wrap_compilation = K (K (K (K (K I))))
   1.110     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.111 @@ -2615,6 +2618,7 @@
   1.112    compilation = Annotated,
   1.113    function_name_prefix = "annotated_",
   1.114    compfuns = PredicateCompFuns.compfuns,
   1.115 +  mk_random = (fn _ => error "no random generation"),
   1.116    modify_funT = I,
   1.117    additional_arguments = K [],
   1.118    wrap_compilation =
   1.119 @@ -2629,6 +2633,7 @@
   1.120    compilation = DSeq,
   1.121    function_name_prefix = "dseq_",
   1.122    compfuns = DSequence_CompFuns.compfuns,
   1.123 +  mk_random = (fn _ => error "no random generation"),
   1.124    modify_funT = I,
   1.125    additional_arguments = K [],
   1.126    wrap_compilation = K (K (K (K (K I))))
   1.127 @@ -2641,6 +2646,17 @@
   1.128    compilation = Pos_Random_DSeq,
   1.129    function_name_prefix = "random_dseq_",
   1.130    compfuns = Random_Sequence_CompFuns.compfuns,
   1.131 +  mk_random = (fn T => fn additional_arguments =>
   1.132 +  let
   1.133 +    val random = Const ("Quickcheck.random_class.random",
   1.134 +      @{typ code_numeral} --> @{typ Random.seed} -->
   1.135 +        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   1.136 +  in
   1.137 +    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   1.138 +      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   1.139 +      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   1.140 +  end),
   1.141 +
   1.142    modify_funT = I,
   1.143    additional_arguments = K [],
   1.144    wrap_compilation = K (K (K (K (K I))))
   1.145 @@ -2653,6 +2669,7 @@
   1.146    compilation = Neg_Random_DSeq,
   1.147    function_name_prefix = "random_dseq_neg_",
   1.148    compfuns = Random_Sequence_CompFuns.compfuns,
   1.149 +  mk_random = (fn _ => error "no random generation"),
   1.150    modify_funT = I,
   1.151    additional_arguments = K [],
   1.152    wrap_compilation = K (K (K (K (K I))))
   1.153 @@ -2683,16 +2700,19 @@
   1.154    comp_modifiers = annotated_comp_modifiers,
   1.155    use_random = false,
   1.156    qname = "annotated_equation"})
   1.157 -(*
   1.158 -val add_quickcheck_equations = gen_add_equations
   1.159 -  (Steps {infer_modes = infer_modes_with_generator,
   1.160 -  define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
   1.161 -  compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
   1.162 +
   1.163 +val add_random_equations = gen_add_equations
   1.164 +  (Steps {
   1.165 +  define_functions =
   1.166 +    fn options => fn preds => fn (s, modes) =>
   1.167 +      define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
   1.168 +      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   1.169 +  comp_modifiers = random_comp_modifiers,
   1.170    prove = prove_by_skip,
   1.171    add_code_equations = K (K I),
   1.172 -  defined = defined_functions Random,
   1.173 +  use_random = true,
   1.174    qname = "random_equation"})
   1.175 -*)
   1.176 +
   1.177  val add_dseq_equations = gen_add_equations
   1.178    (Steps {
   1.179    define_functions =
   1.180 @@ -2777,9 +2797,8 @@
   1.181             | DSeq => add_dseq_equations
   1.182             | Pos_Random_DSeq => add_random_dseq_equations
   1.183             | Depth_Limited => add_depth_limited_equations
   1.184 +           | Random => add_random_equations
   1.185             | compilation => error ("Compilation not supported")
   1.186 -           (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs)
   1.187 -           | Annotated => add_annotated_equations*)
   1.188             ) options [const]))
   1.189        end
   1.190    in
   1.191 @@ -2858,7 +2877,8 @@
   1.192          val additional_arguments =
   1.193            case compilation of
   1.194              Pred => []
   1.195 -          | Random => [@{term "5 :: code_numeral"}]
   1.196 +          | Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
   1.197 +            [@{term "(1, 1) :: code_numeral * code_numeral"}]
   1.198            | Annotated => []
   1.199            | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
   1.200            | DSeq => []
   1.201 @@ -2885,7 +2905,7 @@
   1.202    let
   1.203      val compfuns =
   1.204        case compilation of
   1.205 -        Random => RandomPredCompFuns.compfuns
   1.206 +        Random => PredicateCompFuns.compfuns
   1.207        | DSeq => DSequence_CompFuns.compfuns
   1.208        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
   1.209        | _ => PredicateCompFuns.compfuns
   1.210 @@ -2894,12 +2914,12 @@
   1.211      val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
   1.212      val ts =
   1.213        case compilation of
   1.214 -        Random =>
   1.215 +       (* Random =>
   1.216            fst (Predicate.yieldn k
   1.217            (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
   1.218              (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
   1.219 -            |> Random_Engine.run))
   1.220 -      | Pos_Random_DSeq =>
   1.221 +            |> Random_Engine.run))*)
   1.222 +        Pos_Random_DSeq =>
   1.223            let
   1.224              val [nrandom, size, depth] = arguments
   1.225            in