adding option of evaluating terms after invocation in quickcheck
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 42026da9b58f1db42
parent 42025 cb5b1e85b32e
child 42027 5e40c152c396
adding option of evaluating terms after invocation in quickcheck
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -28,16 +28,16 @@
     1.4    val map_test_params : (typ list * expectation -> typ list * expectation)
     1.5      -> Context.generic -> Context.generic
     1.6    val add_generator:
     1.7 -    string * (Proof.context -> term -> int -> term list option * report option)
     1.8 +    string * (Proof.context -> term * term list -> int -> term list option * report option)
     1.9        -> Context.generic -> Context.generic
    1.10    val add_batch_generator:
    1.11      string * (Proof.context -> term list -> (int -> term list option) list)
    1.12        -> Context.generic -> Context.generic
    1.13    (* testing terms and proof states *)
    1.14 -  val test_term: Proof.context -> bool * bool -> term ->
    1.15 +  val test_term: Proof.context -> bool * bool -> term * term list ->
    1.16      (string * term) list option * ((string * int) list * ((int * report) list) option)
    1.17    val test_goal_terms:
    1.18 -    Proof.context -> bool * bool -> (string * typ) list -> term list
    1.19 +    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list  
    1.20        -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
    1.21    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    1.22    (* testing a batch of terms *)
    1.23 @@ -109,7 +109,7 @@
    1.24  structure Data = Generic_Data
    1.25  (
    1.26    type T =
    1.27 -    ((string * (Proof.context -> term -> int -> term list option * report option)) list
    1.28 +    ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list
    1.29        * (string * (Proof.context -> term list -> (int -> term list option) list)) list)
    1.30        * test_params;
    1.31    val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
    1.32 @@ -182,13 +182,14 @@
    1.33    else
    1.34      f ()
    1.35  
    1.36 -fun test_term ctxt (limit_time, is_interactive) t =
    1.37 +fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    1.38    let
    1.39      val (names, t') = apfst (map fst) (prep_test_term t);
    1.40      val current_size = Unsynchronized.ref 0
    1.41      fun excipit s =
    1.42        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    1.43 -    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
    1.44 +    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    1.45 +      (fn () => mk_tester ctxt (t', eval_terms));
    1.46      fun with_size test_fun k reports =
    1.47        if k > Config.get ctxt size then
    1.48          (NONE, reports)
    1.49 @@ -238,10 +239,11 @@
    1.50  fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
    1.51    let
    1.52      val thy = ProofContext.theory_of ctxt
    1.53 +    val (ts, eval_terms) = split_list ts
    1.54      val (freess, ts') = split_list (map prep_test_term ts)
    1.55      val Ts = map snd (hd freess)
    1.56      val (test_funs, comp_time) = cpu_time "quickcheck compilation"
    1.57 -      (fn () => map (mk_tester ctxt) ts')
    1.58 +      (fn () => map (mk_tester ctxt) (ts' ~~ eval_terms))
    1.59      fun test_card_size (card, size) =
    1.60        (* FIXME: why decrement size by one? *)
    1.61        case fst (the (nth test_funs (card - 1)) (size - 1)) of
    1.62 @@ -290,22 +292,23 @@
    1.63        | subst T = T;
    1.64    in (map_types o map_atyps) subst end;
    1.65  
    1.66 -datatype wellsorted_error = Wellsorted_Error of string | Term of term
    1.67 +datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
    1.68  
    1.69  fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
    1.70    let
    1.71 +    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
    1.72      val thy = ProofContext.theory_of lthy
    1.73      val default_insts =
    1.74        if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
    1.75      val inst_goals =
    1.76 -      map (fn check_goal =>
    1.77 +      map (fn (check_goal, eval_terms) =>
    1.78          if not (null (Term.add_tfree_names check_goal [])) then
    1.79            map (fn T =>
    1.80 -            (pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T)
    1.81 -              check_goal
    1.82 +            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
    1.83 +              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
    1.84                handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
    1.85          else
    1.86 -          [(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals
    1.87 +          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) check_goals
    1.88      val error_msg =
    1.89        cat_lines
    1.90          (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
    1.91 @@ -332,7 +335,7 @@
    1.92        collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals)
    1.93    end;
    1.94  
    1.95 -fun test_goal (time_limit, is_interactive) insts i state =
    1.96 +fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
    1.97    let
    1.98      val lthy = Proof.context_of state;
    1.99      val thy = Proof.theory_of state;
   1.100 @@ -349,9 +352,10 @@
   1.101        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
   1.102      val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
   1.103      val check_goals = case some_locale
   1.104 -     of NONE => [proto_goal]
   1.105 -      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
   1.106 -        (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   1.107 +     of NONE => [(proto_goal, eval_terms)]
   1.108 +      | SOME locale =>
   1.109 +        map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   1.110 +          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   1.111    in
   1.112      test_goal_terms lthy (time_limit, is_interactive) insts check_goals
   1.113    end
   1.114 @@ -398,7 +402,7 @@
   1.115      val res =
   1.116        state
   1.117        |> Proof.map_context (Config.put report false #> Config.put quiet true)
   1.118 -      |> try (test_goal (false, false) [] 1);
   1.119 +      |> try (test_goal (false, false) ([], []) 1);
   1.120    in
   1.121      case res of
   1.122        NONE => (false, state)
   1.123 @@ -471,7 +475,7 @@
   1.124  fun gen_quickcheck args i state =
   1.125    state
   1.126    |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
   1.127 -  |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state'
   1.128 +  |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
   1.129    |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   1.130                 error ("quickcheck expected to find no counterexample but found one") else ()
   1.131             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then