# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID da9b58f1db42a84d7d0de18131f40343e6dd626a
# Parent  cb5b1e85b32e5441af1b5fe6b3bb0b9bdc948adb
adding option of evaluating terms after invocation in quickcheck

diff -r cb5b1e85b32e -r da9b58f1db42 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -28,16 +28,16 @@
   val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
   val add_generator:
-    string * (Proof.context -> term -> int -> term list option * report option)
+    string * (Proof.context -> term * term list -> int -> term list option * report option)
       -> Context.generic -> Context.generic
   val add_batch_generator:
     string * (Proof.context -> term list -> (int -> term list option) list)
       -> Context.generic -> Context.generic
   (* testing terms and proof states *)
-  val test_term: Proof.context -> bool * bool -> term ->
+  val test_term: Proof.context -> bool * bool -> term * term list ->
     (string * term) list option * ((string * int) list * ((int * report) list) option)
   val test_goal_terms:
-    Proof.context -> bool * bool -> (string * typ) list -> term list
+    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list  
       -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
   (* testing a batch of terms *)
@@ -109,7 +109,7 @@
 structure Data = Generic_Data
 (
   type T =
-    ((string * (Proof.context -> term -> int -> term list option * report option)) list
+    ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list
       * (string * (Proof.context -> term list -> (int -> term list option) list)) list)
       * test_params;
   val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
@@ -182,13 +182,14 @@
   else
     f ()
 
-fun test_term ctxt (limit_time, is_interactive) t =
+fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
     val (names, t') = apfst (map fst) (prep_test_term t);
     val current_size = Unsynchronized.ref 0
     fun excipit s =
       "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
-    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
+    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+      (fn () => mk_tester ctxt (t', eval_terms));
     fun with_size test_fun k reports =
       if k > Config.get ctxt size then
         (NONE, reports)
@@ -238,10 +239,11 @@
 fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
   let
     val thy = ProofContext.theory_of ctxt
+    val (ts, eval_terms) = split_list ts
     val (freess, ts') = split_list (map prep_test_term ts)
     val Ts = map snd (hd freess)
     val (test_funs, comp_time) = cpu_time "quickcheck compilation"
-      (fn () => map (mk_tester ctxt) ts')
+      (fn () => map (mk_tester ctxt) (ts' ~~ eval_terms))
     fun test_card_size (card, size) =
       (* FIXME: why decrement size by one? *)
       case fst (the (nth test_funs (card - 1)) (size - 1)) of
@@ -290,22 +292,23 @@
       | subst T = T;
   in (map_types o map_atyps) subst end;
 
-datatype wellsorted_error = Wellsorted_Error of string | Term of term
+datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
 
 fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
   let
+    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
     val thy = ProofContext.theory_of lthy
     val default_insts =
       if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
     val inst_goals =
-      map (fn check_goal =>
+      map (fn (check_goal, eval_terms) =>
         if not (null (Term.add_tfree_names check_goal [])) then
           map (fn T =>
-            (pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T)
-              check_goal
+            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
+              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
               handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
         else
-          [(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals
+          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) check_goals
     val error_msg =
       cat_lines
         (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
@@ -332,7 +335,7 @@
       collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals)
   end;
 
-fun test_goal (time_limit, is_interactive) insts i state =
+fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -349,9 +352,10 @@
       | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
     val check_goals = case some_locale
-     of NONE => [proto_goal]
-      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
-        (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
+     of NONE => [(proto_goal, eval_terms)]
+      | SOME locale =>
+        map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
+          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   in
     test_goal_terms lthy (time_limit, is_interactive) insts check_goals
   end
@@ -398,7 +402,7 @@
     val res =
       state
       |> Proof.map_context (Config.put report false #> Config.put quiet true)
-      |> try (test_goal (false, false) [] 1);
+      |> try (test_goal (false, false) ([], []) 1);
   in
     case res of
       NONE => (false, state)
@@ -471,7 +475,7 @@
 fun gen_quickcheck args i state =
   state
   |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
-  |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state'
+  |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
                error ("quickcheck expected to find no counterexample but found one") else ()
            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then