1.1 --- a/src/Tools/quickcheck.ML	Tue Dec 07 09:36:12 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Tue Dec 07 10:03:43 2010 +0100
     1.3 @@ -192,6 +192,31 @@
     1.4            if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
     1.5    end;
     1.6  
     1.7 +fun test_term_with_increasing_cardinality ctxt is_interactive ts =
     1.8 +  let
     1.9 +    val (namess, ts') = split_list (map prep_test_term ts)
    1.10 +    val (test_funs, comp_time) = cpu_time "quickcheck compilation"
    1.11 +      (fn () => map (mk_tester ctxt) ts')
    1.12 +    fun test_card_size (card, size) =
    1.13 +      (* FIXME: why decrement size by one? *)
    1.14 +      case fst (the (nth test_funs (card - 1)) (size - 1)) of
    1.15 +        SOME ts => SOME ((nth namess (card - 1)) ~~ ts)
    1.16 +      | NONE => NONE
    1.17 +    val enumeration_card_size =
    1.18 +      map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
    1.19 +      |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
    1.20 +    in
    1.21 +      if (forall is_none test_funs) then
    1.22 +        (NONE, ([comp_time], NONE))
    1.23 +      else if (forall is_some test_funs) then
    1.24 +        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
    1.25 +          (get_first test_card_size enumeration_card_size, ([comp_time], NONE))) ()
    1.26 +        handle TimeLimit.TimeOut =>
    1.27 +          if is_interactive then error ("Quickcheck ran out of time") else raise TimeLimit.TimeOut
    1.28 +      else
    1.29 +        error "Unexpectedly, testers of some cardinalities are executable but others are not"       
    1.30 +    end
    1.31 +
    1.32  fun get_finite_types ctxt =
    1.33    fst (chop (Config.get ctxt finite_type_size)
    1.34      (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
    1.35 @@ -223,17 +248,19 @@
    1.36      val default_insts =
    1.37        if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
    1.38      val inst_goals =
    1.39 -      maps (fn check_goal =>
    1.40 +      map (fn check_goal =>
    1.41          if not (null (Term.add_tfree_names check_goal [])) then
    1.42            map (fn T =>
    1.43 -            ((Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
    1.44 -              handle WELLSORTED s => Wellsorted_Error s) default_insts 
    1.45 +            (pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal
    1.46 +              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
    1.47          else
    1.48 -          [Term (Object_Logic.atomize_term thy check_goal)]) check_goals
    1.49 -    val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
    1.50 +          [(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals
    1.51 +    val error_msg = cat_lines (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
    1.52 +    fun is_wellsorted_term (T, Term t) = SOME (T, t)
    1.53 +      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
    1.54      val correct_inst_goals =
    1.55 -      case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
    1.56 -        [] => error error_msg
    1.57 +      case map (map_filter is_wellsorted_term) inst_goals of
    1.58 +        [[]] => error error_msg
    1.59        | xs => xs
    1.60      val _ = if Config.get lthy quiet then () else warning error_msg
    1.61      fun collect_results f reports [] = (NONE, rev reports)
    1.62 @@ -241,7 +268,16 @@
    1.63          case f t of
    1.64            (SOME res, report) => (SOME res, rev (report :: reports))
    1.65          | (NONE, report) => collect_results f (report :: reports) ts
    1.66 -  in collect_results (test_term lthy is_interactive) [] correct_inst_goals end;
    1.67 +    fun test_term' goal =
    1.68 +      case goal of
    1.69 +        [(NONE, t)] => test_term lthy is_interactive t
    1.70 +      | ts => test_term_with_increasing_cardinality lthy is_interactive (map snd ts)                           
    1.71 +  in
    1.72 +    if Config.get lthy finite_types then
    1.73 +      collect_results test_term' [] correct_inst_goals
    1.74 +    else
    1.75 +      collect_results (test_term lthy is_interactive) [] (maps (map snd) correct_inst_goals)
    1.76 +  end;
    1.77  
    1.78  fun test_goal insts i state =
    1.79    let