src/HOL/Tools/Quickcheck/random_generators.ML
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 51551 88d1d19fb74f
     1.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -12,9 +12,9 @@
     1.4      -> seed -> (('a -> 'b) * (unit -> term)) * seed
     1.5    val compile_generator_expr:
     1.6      Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
     1.7 -  val put_counterexample: (unit -> int -> bool -> int -> seed -> (bool * term list) option * seed)
     1.8 +  val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed)
     1.9      -> Proof.context -> Proof.context
    1.10 -  val put_counterexample_report: (unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
    1.11 +  val put_counterexample_report: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
    1.12      -> Proof.context -> Proof.context
    1.13    val instantiate_random_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
    1.14      (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    1.15 @@ -27,9 +27,9 @@
    1.16  (** abstract syntax **)
    1.17  
    1.18  fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
    1.19 -val size = @{term "i::code_numeral"};
    1.20 -val size_pred = @{term "(i::code_numeral) - 1"};
    1.21 -val size' = @{term "j::code_numeral"};
    1.22 +val size = @{term "i::natural"};
    1.23 +val size_pred = @{term "(i::natural) - 1"};
    1.24 +val size' = @{term "j::natural"};
    1.25  val seed = @{term "s::Random.seed"};
    1.26  
    1.27  val resultT =  @{typ "(bool * term list) option"};
    1.28 @@ -76,8 +76,8 @@
    1.29  val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
    1.30  val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
    1.31  
    1.32 -val rew_thms = map mk_meta_eq [@{thm code_numeral_zero_minus_one},
    1.33 -  @{thm Suc_code_numeral_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
    1.34 +val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
    1.35 +  @{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
    1.36  val rew_ts = map (Logic.dest_equals o Thm.prop_of) rew_thms;
    1.37  val rew_ss = HOL_ss addsimps rew_thms;
    1.38  
    1.39 @@ -94,7 +94,7 @@
    1.40      val inst = Thm.instantiate_cterm ([(aT, icT)], []);
    1.41      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
    1.42      val t_rhs = lambda t_k proto_t_rhs;
    1.43 -    val eqs0 = [subst_v @{term "0::code_numeral"} eq,
    1.44 +    val eqs0 = [subst_v @{term "0::natural"} eq,
    1.45        subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
    1.46      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    1.47      val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
    1.48 @@ -189,7 +189,7 @@
    1.49      val rTs = Ts @ Us;
    1.50      fun random_resultT T = @{typ Random.seed}
    1.51        --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
    1.52 -    fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T;
    1.53 +    fun sizeT T = @{typ natural} --> @{typ natural} --> T;
    1.54      val random_auxT = sizeT o random_resultT;
    1.55      val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
    1.56        random_auxsN rTs;
    1.57 @@ -222,9 +222,9 @@
    1.58              tc @{typ Random.seed} (SOME T, @{typ Random.seed});
    1.59          val tk = if is_rec
    1.60            then if k = 0 then size
    1.61 -            else @{term "Quickcheck_Random.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    1.62 -             $ HOLogic.mk_number @{typ code_numeral} k $ size
    1.63 -          else @{term "1::code_numeral"}
    1.64 +            else @{term "Quickcheck_Random.beyond :: natural \<Rightarrow> natural \<Rightarrow> natural"}
    1.65 +             $ HOLogic.mk_number @{typ natural} k $ size
    1.66 +          else @{term "1::natural"}
    1.67        in (is_rec, HOLogic.mk_prod (tk, t)) end;
    1.68      fun sort_rec xs =
    1.69        map_filter (fn (true, t) => SOME t | _ =>  NONE) xs
    1.70 @@ -235,7 +235,7 @@
    1.71      fun mk_select (rT, xs) =
    1.72        mk_const @{const_name Quickcheck_Random.collapse} [@{typ Random.seed}, termifyT rT]
    1.73        $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
    1.74 -        $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
    1.75 +        $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ natural}, random_resultT rT)) xs)
    1.76            $ seed;
    1.77      val auxs_lhss = map (fn t => t $ size $ size' $ seed) random_auxs;
    1.78      val auxs_rhss = map mk_select gen_exprss;
    1.79 @@ -247,8 +247,8 @@
    1.80      val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    1.81      fun mk_size_arg k = case Datatype_Aux.find_shortest_path descr k
    1.82       of SOME (_, l) => if l = 0 then size
    1.83 -          else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    1.84 -            $ HOLogic.mk_number @{typ code_numeral} l $ size
    1.85 +          else @{term "max :: natural \<Rightarrow> natural \<Rightarrow> natural"}
    1.86 +            $ HOLogic.mk_number @{typ natural} l $ size
    1.87        | NONE => size;
    1.88      val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
    1.89        (mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us));
    1.90 @@ -272,7 +272,7 @@
    1.91  
    1.92  structure Counterexample = Proof_Data
    1.93  (
    1.94 -  type T = unit -> int -> bool -> int -> int * int -> (bool * term list) option * (int * int)
    1.95 +  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed
    1.96    (* FIXME avoid user error with non-user text *)
    1.97    fun init _ () = error "Counterexample"
    1.98  );
    1.99 @@ -280,7 +280,7 @@
   1.100  
   1.101  structure Counterexample_Report = Proof_Data
   1.102  (
   1.103 -  type T = unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed
   1.104 +  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed
   1.105    (* FIXME avoid user error with non-user text *)
   1.106    fun init _ () = error "Counterexample_Report"
   1.107  );
   1.108 @@ -318,7 +318,7 @@
   1.109        (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   1.110    in
   1.111      lambda genuine_only
   1.112 -      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   1.113 +      (Abs ("n", @{typ natural}, fold_rev mk_bindclause bounds (return $ check true)))
   1.114    end;
   1.115  
   1.116  fun mk_reporting_generator_expr ctxt (t, _) =
   1.117 @@ -364,21 +364,21 @@
   1.118        (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   1.119    in
   1.120      lambda genuine_only
   1.121 -      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   1.122 +      (Abs ("n", @{typ natural}, fold_rev mk_bindclause bounds (return $ check true)))
   1.123    end
   1.124  
   1.125  val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   1.126    ((mk_generator_expr, 
   1.127 -    absdummy @{typ bool} (absdummy @{typ code_numeral}
   1.128 +    absdummy @{typ bool} (absdummy @{typ natural}
   1.129        @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
   1.130 -    @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
   1.131 +    @{typ "bool => natural => Random.seed => (bool * term list) option * Random.seed"})
   1.132  
   1.133  val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   1.134    ((mk_reporting_generator_expr,
   1.135 -    absdummy @{typ bool} (absdummy @{typ code_numeral}
   1.136 +    absdummy @{typ bool} (absdummy @{typ natural}
   1.137        @{term "Pair (None, ([], False)) :: Random.seed =>
   1.138          ((bool * term list) option * (bool list * bool)) * Random.seed"})),
   1.139 -    @{typ "bool => code_numeral => Random.seed => ((bool * term list) option * (bool list * bool)) * Random.seed"})
   1.140 +    @{typ "bool => natural => Random.seed => ((bool * term list) option * (bool list * bool)) * Random.seed"})
   1.141      
   1.142      
   1.143  (* single quickcheck report *)
   1.144 @@ -402,7 +402,7 @@
   1.145  val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
   1.146    satisfied_assms = [], positive_concl_tests = 0 }
   1.147      
   1.148 -fun compile_generator_expr ctxt ts =
   1.149 +fun compile_generator_expr_raw ctxt ts =
   1.150    let
   1.151      val thy = Proof_Context.theory_of ctxt
   1.152      val iterations = Config.get ctxt Quickcheck.iterations
   1.153 @@ -449,6 +449,13 @@
   1.154        end
   1.155    end;
   1.156  
   1.157 +fun compile_generator_expr ctxt ts =
   1.158 +  let
   1.159 +    val compiled = compile_generator_expr_raw ctxt ts
   1.160 +  in fn genuine_only => fn [card, size] =>
   1.161 +    compiled genuine_only [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
   1.162 +  end;
   1.163 +
   1.164  val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
   1.165    @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
   1.166