src/HOL/Tools/Quickcheck/random_generators.ML
changeset 50818 5d4852f1b952
parent 50723 07ecb6716df2
child 51126 df86080de4cb
equal deleted inserted replaced
50817:652731d92061 50818:5d4852f1b952
   447         fn genuine_only => fn [card, size] =>
   447         fn genuine_only => fn [card, size] =>
   448           (rpair NONE (iterate genuine_only (card, size) iterations))
   448           (rpair NONE (iterate genuine_only (card, size) iterations))
   449       end
   449       end
   450   end;
   450   end;
   451 
   451 
   452 fun size_matters_for _ Ts = not (forall
   452 val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
   453   (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
   453   @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
   454     (*FIXME eliminate dynamic name reference*)
   454 
       
   455 fun size_matters_for _ Ts =
       
   456   not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts);
   455 
   457 
   456 val test_goals =
   458 val test_goals =
   457   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
   459   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
   458   
   460   
   459 (** setup **)
   461 (** setup **)