passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 42028bd6515e113b2
parent 42027 5e40c152c396
child 42029 da92153d6dff
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/inductive_codegen.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -211,6 +211,61 @@
     1.4  
     1.5  (** building and compiling generator expressions **)
     1.6  
     1.7 +fun mk_generator_expr ctxt (t, eval_terms) =
     1.8 +  let
     1.9 +    val thy = ProofContext.theory_of ctxt
    1.10 +    val ctxt' = Variable.auto_fixes t ctxt
    1.11 +    val names = Term.add_free_names t []
    1.12 +    val frees = map Free (Term.add_frees t [])
    1.13 +    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
    1.14 +    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
    1.15 +    val depth = Free (depth_name, @{typ code_numeral})
    1.16 +    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
    1.17 +    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
    1.18 +    val appendC = @{term "List.append :: term list => term list => term list"}  
    1.19 +    val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $
    1.20 +      (HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms)))
    1.21 +    fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
    1.22 +      if Sign.of_sort thy (T, @{sort enum}) then
    1.23 +        Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
    1.24 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    1.25 +            $ lambda free (lambda term_var t))
    1.26 +      else
    1.27 +        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    1.28 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
    1.29 +            $ lambda free (lambda term_var t)) $ depth
    1.30 +    val none_t = @{term "None :: term list option"}
    1.31 +    fun mk_safe_if (cond, then_t, else_t) =
    1.32 +      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
    1.33 +        (@{term "If :: bool => term list option => term list option => term list option"}
    1.34 +        $ cond $ then_t $ else_t) $ none_t;
    1.35 +    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    1.36 +        | strip_imp A = ([], A)
    1.37 +    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    1.38 +    fun mk_naive_test_term t =
    1.39 +      fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return)) 
    1.40 +    fun mk_smart_test_term' concl bound_vars assms =
    1.41 +      let
    1.42 +        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
    1.43 +        val (vars, check) =
    1.44 +          case assms of [] => (vars_of concl, (concl, none_t, return))
    1.45 +            | assm :: assms => (vars_of assm, (assm,
    1.46 +                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
    1.47 +      in
    1.48 +        fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
    1.49 +      end
    1.50 +    fun mk_smart_test_term t =
    1.51 +      let
    1.52 +        val (assms, concl) = strip_imp t
    1.53 +      in
    1.54 +        mk_smart_test_term' concl [] assms
    1.55 +      end
    1.56 +    val mk_test_term =
    1.57 +      if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
    1.58 +  in lambda depth (mk_test_term t) end
    1.59 +
    1.60 +(** generator compiliation **)
    1.61 +
    1.62  structure Counterexample = Proof_Data
    1.63  (
    1.64    type T = unit -> int -> term list option
    1.65 @@ -229,76 +284,10 @@
    1.66  
    1.67  val target = "Quickcheck";
    1.68  
    1.69 -fun mk_smart_generator_expr ctxt t =
    1.70 -  let
    1.71 -    val thy = ProofContext.theory_of ctxt
    1.72 -    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
    1.73 -    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
    1.74 -    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
    1.75 -    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
    1.76 -    val depth = Free (depth_name, @{typ code_numeral})
    1.77 -    val frees = map2 (curry Free) names Ts
    1.78 -    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
    1.79 -    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    1.80 -      | strip_imp A = ([], A)
    1.81 -    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
    1.82 -    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
    1.83 -    fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
    1.84 -      if Sign.of_sort thy (T, @{sort enum}) then
    1.85 -        Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
    1.86 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    1.87 -            $ lambda free (lambda term_var t))
    1.88 -      else
    1.89 -        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    1.90 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    1.91 -            $ lambda free (lambda term_var t)) $ depth
    1.92 -    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    1.93 -    val none_t = @{term "None :: term list option"}
    1.94 -    fun mk_safe_if (cond, then_t, else_t) =
    1.95 -      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
    1.96 -        (@{term "If :: bool => term list option => term list option => term list option"}
    1.97 -        $ cond $ then_t $ else_t) $ none_t;
    1.98 -    fun mk_test_term bound_vars assms =
    1.99 -      let
   1.100 -        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   1.101 -        val (vars, check) =
   1.102 -          case assms of [] =>
   1.103 -            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
   1.104 -          | assm :: assms =>
   1.105 -            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
   1.106 -      in
   1.107 -        fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   1.108 -      end
   1.109 -  in lambda depth (mk_test_term [] assms) end
   1.110 -
   1.111 -fun mk_generator_expr ctxt t =
   1.112 -  let
   1.113 -    val Ts = (map snd o fst o strip_abs) t;
   1.114 -    val thy = ProofContext.theory_of ctxt
   1.115 -    val bound_max = length Ts - 1;
   1.116 -    val bounds = map_index (fn (i, ty) =>
   1.117 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   1.118 -    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
   1.119 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   1.120 -    val check =
   1.121 -      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   1.122 -        (@{term "If :: bool => term list option => term list option => term list option"}
   1.123 -        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   1.124 -      $ @{term "None :: term list option"};
   1.125 -    fun mk_exhaustive_closure (_, _, i, T) t =
   1.126 -      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   1.127 -        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   1.128 -        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   1.129 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_exhaustive_closure bounds check) end
   1.130 -
   1.131 -(** generator compiliation **)
   1.132 -
   1.133  fun compile_generator_expr ctxt (t, eval_terms) =
   1.134    let
   1.135      val thy = ProofContext.theory_of ctxt
   1.136 -    val t' =
   1.137 -      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
   1.138 -        ctxt t;
   1.139 +    val t' = mk_generator_expr ctxt (t, eval_terms);
   1.140      val compile = Code_Runtime.dynamic_value_strict
   1.141        (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   1.142        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   1.143 @@ -311,9 +300,7 @@
   1.144  fun compile_generator_exprs ctxt ts =
   1.145    let
   1.146      val thy = ProofContext.theory_of ctxt
   1.147 -    val mk_generator_expr =
   1.148 -      if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
   1.149 -    val ts' = map (mk_generator_expr ctxt) ts;
   1.150 +    val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
   1.151      val compiles = Code_Runtime.dynamic_value_strict
   1.152        (Counterexample_Batch.get, put_counterexample_batch,
   1.153          "Exhaustive_Generators.put_counterexample_batch")
   1.154 @@ -323,7 +310,7 @@
   1.155      map (fn compile => fn size => compile size
   1.156        |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   1.157    end;
   1.158 -  
   1.159 +
   1.160    
   1.161  (** setup **)
   1.162  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     2.3 @@ -216,12 +216,13 @@
     2.4  fun compile_generator_expr ctxt (t, eval_terms) size =
     2.5    let
     2.6      val thy = ProofContext.theory_of ctxt
     2.7 -    val t' = if Config.get ctxt finite_functions then finitize_functions t else t
     2.8 +    val t' = list_abs_free (Term.add_frees t [], t)
     2.9 +    val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
    2.10      fun ensure_testable t =
    2.11        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    2.12      val result = dynamic_value_strict
    2.13        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    2.14 -      thy (Option.map o map) (ensure_testable t') [] size
    2.15 +      thy (Option.map o map) (ensure_testable t'') [] size
    2.16    in
    2.17      (result, NONE)
    2.18    end;
     3.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     3.3 @@ -377,16 +377,17 @@
     3.4      
     3.5  fun compile_generator_expr ctxt (t, eval_terms) =
     3.6    let
     3.7 -    val Ts = (map snd o fst o strip_abs) t;
     3.8 +    val t' = list_abs_free (Term.add_frees t [], t)
     3.9 +    val Ts = (map snd o fst o strip_abs) t';
    3.10      val thy = ProofContext.theory_of ctxt
    3.11      val iterations = Config.get ctxt Quickcheck.iterations
    3.12    in
    3.13      if Config.get ctxt Quickcheck.report then
    3.14        let
    3.15 -        val t' = mk_reporting_generator_expr thy t Ts;
    3.16 +        val t'' = mk_reporting_generator_expr thy t' Ts;
    3.17          val compile = Code_Runtime.dynamic_value_strict
    3.18            (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
    3.19 -          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
    3.20 +          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t'' [];
    3.21          val single_tester = compile #> Random_Engine.run
    3.22          fun iterate_and_collect size 0 report = (NONE, report)
    3.23            | iterate_and_collect size j report =
    3.24 @@ -404,10 +405,10 @@
    3.25        end
    3.26      else
    3.27        let
    3.28 -        val t' = mk_generator_expr thy t Ts;
    3.29 +        val t'' = mk_generator_expr thy t' Ts;
    3.30          val compile = Code_Runtime.dynamic_value_strict
    3.31            (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
    3.32 -          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
    3.33 +          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t'' [];
    3.34          val single_tester = compile #> Random_Engine.run
    3.35          fun iterate size 0 = NONE
    3.36            | iterate size j =
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Mar 18 18:19:42 2011 +0100
     4.3 @@ -810,8 +810,9 @@
     4.4  
     4.5  fun test_term ctxt (t, []) =
     4.6    let
     4.7 +    val t' = list_abs_free (Term.add_frees t [], t)
     4.8      val thy = ProofContext.theory_of ctxt;
     4.9 -    val (xs, p) = strip_abs t;
    4.10 +    val (xs, p) = strip_abs t';
    4.11      val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
    4.12      val args = map Free args';
    4.13      val (ps, q) = strip_imp p;
     5.1 --- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     5.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     5.3 @@ -35,10 +35,10 @@
     5.4        -> Context.generic -> Context.generic
     5.5    (* testing terms and proof states *)
     5.6    val test_term: Proof.context -> bool * bool -> term * term list ->
     5.7 -    (string * term) list option * ((string * int) list * ((int * report) list) option)
     5.8 +    ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option)
     5.9    val test_goal_terms:
    5.10      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list  
    5.11 -      -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
    5.12 +      -> ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option) list
    5.13    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    5.14    (* testing a batch of terms *)
    5.15    val test_terms: Proof.context -> term list -> (string * term) list option list option
    5.16 @@ -158,14 +158,13 @@
    5.17    
    5.18  (* testing propositions *)
    5.19  
    5.20 -fun prep_test_term t =
    5.21 +fun check_test_term t =
    5.22    let
    5.23      val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    5.24        error "Term to be tested contains type variables";
    5.25      val _ = null (Term.add_vars t []) orelse
    5.26        error "Term to be tested contains schematic variables";
    5.27 -    val frees = Term.add_frees t [];
    5.28 -  in (frees, list_abs_free (frees, t)) end
    5.29 +  in () end
    5.30  
    5.31  fun cpu_time description f =
    5.32    let
    5.33 @@ -182,14 +181,22 @@
    5.34    else
    5.35      f ()
    5.36  
    5.37 +fun mk_result names eval_terms ts =
    5.38 +  let
    5.39 +    val (ts1, ts2) = chop (length names) ts
    5.40 +  in
    5.41 +    (names ~~ ts1, eval_terms ~~ ts2) 
    5.42 +  end
    5.43 +
    5.44  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    5.45    let
    5.46 -    val (names, t') = apfst (map fst) (prep_test_term t);
    5.47 +    val _ = check_test_term t
    5.48 +    val names = Term.add_free_names t []
    5.49      val current_size = Unsynchronized.ref 0
    5.50      fun excipit s =
    5.51        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    5.52      val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    5.53 -      (fn () => mk_tester ctxt (t', eval_terms));
    5.54 +      (fn () => mk_tester ctxt (t, eval_terms));
    5.55      fun with_size test_fun k reports =
    5.56        if k > Config.get ctxt size then
    5.57          (NONE, reports)
    5.58 @@ -212,7 +219,7 @@
    5.59              val ((result, reports), exec_time) =
    5.60                cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
    5.61            in
    5.62 -            (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
    5.63 +            (Option.map (mk_result names eval_terms) result,
    5.64                ([exec_time, comp_time],
    5.65                 if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
    5.66            end) (fn () => error (excipit "ran out of time")) ()
    5.67 @@ -220,8 +227,9 @@
    5.68  
    5.69  fun test_terms ctxt ts =
    5.70    let
    5.71 -    val (namess, ts') = split_list (map (fn t => apfst (map fst) (prep_test_term t)) ts)
    5.72 -    val test_funs = mk_batch_tester ctxt ts'
    5.73 +    val _ = map check_test_term ts
    5.74 +    val namess = map (fn t => Term.add_free_names t []) ts
    5.75 +    val test_funs = mk_batch_tester ctxt ts
    5.76      fun with_size tester k =
    5.77        if k > Config.get ctxt size then NONE
    5.78        else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
    5.79 @@ -240,14 +248,15 @@
    5.80    let
    5.81      val thy = ProofContext.theory_of ctxt
    5.82      val (ts, eval_terms) = split_list ts
    5.83 -    val (freess, ts') = split_list (map prep_test_term ts)
    5.84 -    val Ts = map snd (hd freess)
    5.85 +    val _ = map check_test_term ts
    5.86 +    val names = Term.add_free_names (hd ts) []
    5.87 +    val Ts = map snd (Term.add_frees (hd ts) [])
    5.88      val (test_funs, comp_time) = cpu_time "quickcheck compilation"
    5.89 -      (fn () => map (mk_tester ctxt) (ts' ~~ eval_terms))
    5.90 +      (fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
    5.91      fun test_card_size (card, size) =
    5.92        (* FIXME: why decrement size by one? *)
    5.93        case fst (the (nth test_funs (card - 1)) (size - 1)) of
    5.94 -        SOME ts => SOME (map fst (nth freess (card - 1)) ~~ ts)
    5.95 +        SOME ts => SOME (mk_result names (nth eval_terms (card - 1)) ts)
    5.96        | NONE => NONE
    5.97      val enumeration_card_size =
    5.98        if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
    5.99 @@ -365,10 +374,14 @@
   5.100  fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
   5.101  
   5.102  fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
   5.103 -  | pretty_counterex ctxt auto (SOME cex) =
   5.104 -      Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
   5.105 +  | pretty_counterex ctxt auto (SOME (cex, eval_terms)) =
   5.106 +      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
   5.107          map (fn (s, t) =>
   5.108 -          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex));
   5.109 +          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
   5.110 +        @ (Pretty.str ("Evaluated terms:\n") ::
   5.111 +        map (fn (t, u) =>
   5.112 +          Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
   5.113 +          (rev eval_terms)));
   5.114  
   5.115  fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
   5.116      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
   5.117 @@ -481,7 +494,7 @@
   5.118             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
   5.119                 error ("quickcheck expected to find a counterexample but did not find one") else ()))
   5.120  
   5.121 -fun quickcheck args i state = fst (gen_quickcheck args i state);
   5.122 +fun quickcheck args i state = Option.map fst (fst (gen_quickcheck args i state));
   5.123  
   5.124  fun quickcheck_cmd args i state =
   5.125    gen_quickcheck args i (Toplevel.proof_of state)