adding post-processing of terms to narrowing-based Quickcheck
authorbulwahn
Thu Sep 22 07:26:53 2011 +0200 (2011-09-22)
changeset 45039632a033616e9
parent 45038 e24bf05dd273
child 45040 8570623e3b6d
adding post-processing of terms to narrowing-based Quickcheck
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 21 17:43:13 2011 -0700
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Sep 22 07:26:53 2011 +0200
     1.3 @@ -353,6 +353,19 @@
     1.4      (names ~~ boundTs', t')
     1.5    end
     1.6  
     1.7 +fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT)
     1.8 +
     1.9 +fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) =
    1.10 +    absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
    1.11 +  | eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) =
    1.12 +    let
    1.13 +      val (T1, T2) = dest_ffun (body_type T)
    1.14 +    in
    1.15 +      Quickcheck_Common.mk_fun_upd T1 T2
    1.16 +        (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
    1.17 +    end
    1.18 +  | eval_finite_functions t = t
    1.19 +
    1.20  (** tester **)
    1.21  
    1.22  val rewrs =
    1.23 @@ -389,12 +402,15 @@
    1.24    | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
    1.25      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
    1.26  
    1.27 +val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions
    1.28 +
    1.29  fun mk_terms ctxt qs result =
    1.30    let
    1.31      val
    1.32        ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
    1.33      in
    1.34        map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
    1.35 +      |> map (apsnd post_process)
    1.36      end
    1.37    
    1.38  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    1.39 @@ -436,7 +452,8 @@
    1.40            thy (apfst o Option.map o map) (ensure_testable (finitize t'))
    1.41        in
    1.42          Quickcheck.Result
    1.43 -         {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
    1.44 +         {counterexample =
    1.45 +           Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process) counterexample,
    1.46            evaluation_terms = Option.map (K []) counterexample,
    1.47            timings = #timings (dest_result result), reports = #reports (dest_result result)}
    1.48        end
     2.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Sep 21 17:43:13 2011 -0700
     2.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Sep 22 07:26:53 2011 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    val gen_mk_parametric_generator_expr :
     2.5     (((Proof.context -> term * term list -> term) * term) * typ)
     2.6       -> Proof.context -> (term * term list) list -> term
     2.7 +  val mk_fun_upd : typ -> typ -> term * term -> term -> term
     2.8    val post_process_term : term -> term
     2.9  end;
    2.10