adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
authorbulwahn
Tue Jun 07 11:11:01 2011 +0200 (2011-06-07)
changeset 43240da47097bd589
parent 43239 42f82fda796b
child 43241 93b1183e43e5
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 07 11:10:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 07 11:11:01 2011 +0200
     1.3 @@ -299,9 +299,9 @@
     1.4  
     1.5  val put_counterexample = Counterexample.put
     1.6  
     1.7 -fun finitize_functions t =
     1.8 +fun finitize_functions (xTs, t) =
     1.9    let
    1.10 -    val ((names, Ts), t') = apfst split_list (strip_abs t)
    1.11 +    val (names, boundTs) = split_list xTs
    1.12      fun mk_eval_ffun dT rT =
    1.13        Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
    1.14          Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
    1.15 @@ -320,17 +320,19 @@
    1.16              Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
    1.17        end
    1.18        | eval_function T = (I, T)
    1.19 -    val (tt, Ts') = split_list (map eval_function Ts)
    1.20 -    val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t')
    1.21 +    val (tt, boundTs') = split_list (map eval_function boundTs)
    1.22 +    val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)
    1.23    in
    1.24 -    list_abs (names ~~ Ts', t'')
    1.25 +    (names ~~ boundTs', t')
    1.26    end
    1.27  
    1.28  (** tester **)
    1.29  
    1.30  val rewrs =
    1.31 -  map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) (@{thms all_simps} @ @{thms ex_simps})
    1.32 -    @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) [@{thm not_ex}, @{thm not_all}]
    1.33 +    map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
    1.34 +      (@{thms all_simps} @ @{thms ex_simps})
    1.35 +    @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
    1.36 +        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}]
    1.37  
    1.38  fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
    1.39  
    1.40 @@ -355,7 +357,6 @@
    1.41        (list_comb (t , map Bound (((length qs) - 1) downto 0))))
    1.42    end
    1.43  
    1.44 -  
    1.45  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
    1.46      fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
    1.47        (t, mk_case_term ctxt (p - 1) qs' c)) cs))
    1.48 @@ -378,8 +379,12 @@
    1.49    in
    1.50      if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
    1.51        let
    1.52 -        val (qs, t') = strip_quantifiers pnf_t
    1.53 -        val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs t'
    1.54 +        fun wrap f (qs, t) =
    1.55 +          let val (qs1, qs2) = split_list qs in
    1.56 +          apfst (map2 pair qs1) (f (qs2, t)) end
    1.57 +        val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.58 +        val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
    1.59 +        val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
    1.60          val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
    1.61            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    1.62          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    1.63 @@ -392,18 +397,20 @@
    1.64          Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
    1.65            timings = [], reports = []}
    1.66        end
    1.67 -    else (let
    1.68 -      val t' = HOLogic.list_all (Term.add_frees t [], t)
    1.69 -      val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
    1.70 -      fun ensure_testable t =
    1.71 -        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.72 -      val result = dynamic_value_strict false
    1.73 -        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.74 -        thy (Option.map o map) (ensure_testable t'')
    1.75 -    in
    1.76 -      Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
    1.77 -        evaluation_terms = Option.map (K []) result, timings = [], reports = []}
    1.78 -    end)
    1.79 +    else
    1.80 +      let
    1.81 +        val t' = Term.list_abs_free (Term.add_frees t [], t)
    1.82 +        fun wrap f t = list_abs (f (strip_abs t))
    1.83 +        val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.84 +        fun ensure_testable t =
    1.85 +          Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.86 +        val result = dynamic_value_strict false
    1.87 +          (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.88 +          thy (Option.map o map) (ensure_testable (finitize t'))
    1.89 +      in
    1.90 +        Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
    1.91 +          evaluation_terms = Option.map (K []) result, timings = [], reports = []}
    1.92 +      end
    1.93    end;
    1.94  
    1.95  fun test_goals ctxt (limit_time, is_interactive) insts goals =