1.1 --- a/src/Tools/quickcheck.ML	Mon Nov 22 11:34:53 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 22 11:34:54 2010 +0100
     1.3 @@ -16,6 +16,8 @@
     1.4    val report : bool Config.T
     1.5    val quiet : bool Config.T
     1.6    val timeout : real Config.T
     1.7 +  val finite_types : bool Config.T
     1.8 +  val finite_type_size : int Config.T
     1.9    datatype report = Report of
    1.10      { iterations : int, raised_match_errors : int,
    1.11        satisfied_assms : int list, positive_concl_tests : int }
    1.12 @@ -32,6 +34,9 @@
    1.13      (string * term) list option * ((string * int) list * ((int * report list) list) option)
    1.14    val test_term: Proof.context -> string option -> term ->
    1.15      (string * term) list option * ((string * int) list * ((int * report list) list) option)
    1.16 +  val test_goal_terms:
    1.17 +    Proof.context -> string option * (string * typ) list -> term list
    1.18 +      -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
    1.19    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    1.20  end;
    1.21  
    1.22 @@ -199,6 +204,10 @@
    1.23       apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
    1.24     end
    1.25  
    1.26 +(* we actually assume we know the generators and its behaviour *)
    1.27 +fun is_iteratable "small" = false
    1.28 +  | is_iteratable "random" = true
    1.29 +  
    1.30  fun test_term ctxt generator_name t =
    1.31    let
    1.32      val (names, t') = prep_test_term t;
    1.33 @@ -223,15 +232,24 @@
    1.34        satisfied_assms = [], positive_concl_tests = 0 }
    1.35      fun with_testers k [] = (NONE, [])
    1.36        | with_testers k (tester :: testers) =
    1.37 -          case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report
    1.38 +        let
    1.39 +          val niterations = case generator_name of
    1.40 +            SOME generator_name =>
    1.41 +              if is_iteratable generator_name then Config.get ctxt iterations else 1
    1.42 +          | NONE => Config.get ctxt iterations
    1.43 +          val (result, timing) = cpu_time ("size " ^ string_of_int k)
    1.44 +            (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
    1.45 +        in
    1.46 +          case result
    1.47             of (NONE, report) => apsnd (cons report) (with_testers k testers)
    1.48 -            | (SOME q, report) => (SOME q, [report]);
    1.49 +            | (SOME q, report) => (SOME q, [report])
    1.50 +        end
    1.51      fun with_size k reports =
    1.52        if k > Config.get ctxt size then (NONE, reports)
    1.53        else
    1.54         (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
    1.55          let
    1.56 -          val _ = current_size := k  
    1.57 +          val _ = current_size := k
    1.58            val (result, new_report) = with_testers k testers
    1.59            val reports = ((k, new_report) :: reports)
    1.60          in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
    1.61 @@ -272,26 +290,9 @@
    1.62  
    1.63  datatype wellsorted_error = Wellsorted_Error of string | Term of term
    1.64  
    1.65 -fun test_goal (generator_name, insts) i state =
    1.66 +fun test_goal_terms lthy (generator_name, insts) check_goals =
    1.67    let
    1.68 -    val lthy = Proof.context_of state;
    1.69 -    val thy = Proof.theory_of state;
    1.70 -    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
    1.71 -      | strip t = t;
    1.72 -    val {goal = st, ...} = Proof.raw_goal state;
    1.73 -    val (gi, frees) = Logic.goal_params (prop_of st) i;
    1.74 -    val some_locale = case (Option.map #target o Named_Target.peek) lthy
    1.75 -     of NONE => NONE
    1.76 -      | SOME "" => NONE
    1.77 -      | SOME locale => SOME locale;
    1.78 -    val assms = if Config.get lthy no_assms then [] else case some_locale
    1.79 -     of NONE => Assumption.all_assms_of lthy
    1.80 -      | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
    1.81 -    val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
    1.82 -    val check_goals = case some_locale
    1.83 -     of NONE => [proto_goal]
    1.84 -      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
    1.85 -        (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
    1.86 +    val thy = ProofContext.theory_of lthy 
    1.87      val inst_goals =
    1.88        if Config.get lthy finite_types then 
    1.89          maps (fn check_goal => map (fn T =>
    1.90 @@ -314,6 +315,30 @@
    1.91          | (NONE, report) => collect_results f (report :: reports) ts
    1.92    in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
    1.93  
    1.94 +fun test_goal (generator_name, insts) i state =
    1.95 +  let
    1.96 +    val lthy = Proof.context_of state;
    1.97 +    val thy = Proof.theory_of state;
    1.98 +    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
    1.99 +      | strip t = t;
   1.100 +    val {goal = st, ...} = Proof.raw_goal state;
   1.101 +    val (gi, frees) = Logic.goal_params (prop_of st) i;
   1.102 +    val some_locale = case (Option.map #target o Named_Target.peek) lthy
   1.103 +     of NONE => NONE
   1.104 +      | SOME "" => NONE
   1.105 +      | SOME locale => SOME locale;
   1.106 +    val assms = if Config.get lthy no_assms then [] else case some_locale
   1.107 +     of NONE => Assumption.all_assms_of lthy
   1.108 +      | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
   1.109 +    val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
   1.110 +    val check_goals = case some_locale
   1.111 +     of NONE => [proto_goal]
   1.112 +      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
   1.113 +        (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   1.114 +  in
   1.115 +    test_goal_terms lthy (generator_name, insts) check_goals
   1.116 +  end
   1.117 +
   1.118  (* pretty printing *)
   1.119  
   1.120  fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"