--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 19 20:10:59 2014 +0100
@@ -1682,56 +1682,45 @@
(* transformation for code generation *)
-(* FIXME just one data slot (record) per program unit *)
-
-structure Pred_Result = Proof_Data
-(
- type T = unit -> term Predicate.pred
- fun init _ () = raise Fail "Pred_Result"
-);
-val put_pred_result = Pred_Result.put;
-
-structure Pred_Random_Result = Proof_Data
-(
- type T = unit -> seed -> term Predicate.pred * seed
- fun init _ () = raise Fail "Pred_Random_Result"
-);
-val put_pred_random_result = Pred_Random_Result.put;
-
-structure Dseq_Result = Proof_Data
-(
- type T = unit -> term Limited_Sequence.dseq
- fun init _ () = raise Fail "Dseq_Result"
-);
-val put_dseq_result = Dseq_Result.put;
-
-structure Dseq_Random_Result = Proof_Data
+structure Data = Proof_Data
(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed
- fun init _ () = raise Fail "Dseq_Random_Result"
+ type T =
+ (unit -> term Predicate.pred) *
+ (unit -> seed -> term Predicate.pred * seed) *
+ (unit -> term Limited_Sequence.dseq) *
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ term Limited_Sequence.dseq * seed) *
+ (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence);
+ val empty: T =
+ (fn () => raise Fail "pred_result",
+ fn () => raise Fail "pred_random_result",
+ fn () => raise Fail "dseq_result",
+ fn () => raise Fail "dseq_random_result",
+ fn () => raise Fail "new_dseq_result",
+ fn () => raise Fail "lseq_random_result",
+ fn () => raise Fail "lseq_random_stats_result");
+ fun init _ = empty;
);
-val put_dseq_random_result = Dseq_Random_Result.put;
-
-structure New_Dseq_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
- fun init _ () = raise Fail "New_Dseq_Random_Result"
-);
-val put_new_dseq_result = New_Dseq_Result.put;
-structure Lseq_Random_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
- fun init _ () = raise Fail "Lseq_Random_Result"
-);
-val put_lseq_random_result = Lseq_Random_Result.put;
+val get_pred_result = #1 o Data.get;
+val get_pred_random_result = #2 o Data.get;
+val get_dseq_result = #3 o Data.get;
+val get_dseq_random_result = #4 o Data.get;
+val get_new_dseq_result = #5 o Data.get;
+val get_lseq_random_result = #6 o Data.get;
+val get_lseq_random_stats_result = #7 o Data.get;
-structure Lseq_Random_Stats_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence
- fun init _ () = raise Fail "Lseq_Random_Stats_Result"
-);
-val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
+val put_pred_result = Data.map o @{apply 7(1)} o K;
+val put_pred_random_result = Data.map o @{apply 7(2)} o K;
+val put_dseq_result = Data.map o @{apply 7(3)} o K;
+val put_dseq_random_result = Data.map o @{apply 7(4)} o K;
+val put_new_dseq_result = Data.map o @{apply 7(5)} o K;
+val put_lseq_random_result = Data.map o @{apply 7(6)} o K;
+val put_lseq_random_stats_result = Data.map o @{apply 7(7)} o K;
fun dest_special_compr t =
let
@@ -1906,24 +1895,32 @@
val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
in
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
- (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
- ctxt NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
+ (Code_Runtime.dynamic_value_strict
+ (get_dseq_random_result, put_dseq_random_result,
+ "Predicate_Compile_Core.put_dseq_random_result")
+ ctxt NONE
+ (fn proc => fn g => fn nrandom => fn size => fn s =>
+ g nrandom size s |>> Limited_Sequence.map proc)
t' [] nrandom size
|> Random_Engine.run)
depth true)) ())
end
| DSeq =>
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
- (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
- ctxt NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
+ (Code_Runtime.dynamic_value_strict
+ (get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+ ctxt NONE Limited_Sequence.map t' [])
+ (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
| Pos_Generator_DSeq =>
let
val depth = Code_Numeral.natural_of_integer (the_single arguments)
in
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
- (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
- ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
- t' [] depth))) ())
+ (Code_Runtime.dynamic_value_strict
+ (get_new_dseq_result, put_new_dseq_result,
+ "Predicate_Compile_Core.put_new_dseq_result")
+ ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
+ t' [] depth))) ())
end
| New_Pos_Random_DSeq =>
let
@@ -1935,23 +1932,28 @@
(split_list (TimeLimit.timeLimit time_limit
(fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
- (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
+ (get_lseq_random_stats_result, put_lseq_random_stats_result,
+ "Predicate_Compile_Core.put_lseq_random_stats_result")
ctxt NONE
- (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+ (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+ g nrandom size s depth
|> Lazy_Sequence.map (apfst proc))
t' [] nrandom size seed depth))) ()))
else rpair NONE
(TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
- (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
- ctxt NONE
- (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
- |> Lazy_Sequence.map proc)
- t' [] nrandom size seed depth))) ())
+ (get_lseq_random_result, put_lseq_random_result,
+ "Predicate_Compile_Core.put_lseq_random_result")
+ ctxt NONE
+ (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+ g nrandom size s depth
+ |> Lazy_Sequence.map proc)
+ t' [] nrandom size seed depth))) ())
end
| _ =>
rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
- (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+ (Code_Runtime.dynamic_value_strict
+ (get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
ctxt NONE Predicate.map t' []))) ()))
handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
in ((T, ts), statistics) end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 19 20:10:59 2014 +0100
@@ -40,45 +40,37 @@
type seed = Random_Engine.seed;
-(* FIXME just one data slot (record) per program unit *)
-
-structure Pred_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
- Code_Numeral.natural -> seed -> term list Predicate.pred
- fun init _ () = raise Fail "Pred_Result"
-)
-val put_pred_result = Pred_Result.put
-
-structure Dseq_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
- seed -> term list Limited_Sequence.dseq * seed
- fun init _ () = raise Fail "Dseq_Result"
-)
-val put_dseq_result = Dseq_Result.put
-
-structure Lseq_Result = Proof_Data
+structure Data = Proof_Data
(
- type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
- seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
- fun init _ () = raise Fail "Lseq_Result"
-)
-val put_lseq_result = Lseq_Result.put
+ type T =
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+ Code_Numeral.natural -> seed -> term list Predicate.pred) *
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+ seed -> term list Limited_Sequence.dseq * seed) *
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+ seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) *
+ (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) *
+ (unit -> Code_Numeral.natural -> (bool * term list) option);
+ val empty: T =
+ (fn () => raise Fail "pred_result",
+ fn () => raise Fail "dseq_result",
+ fn () => raise Fail "lseq_result",
+ fn () => raise Fail "new_dseq_result",
+ fn () => raise Fail "cps_result");
+ fun init _ = empty;
+);
-structure New_Dseq_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
- fun init _ () = raise Fail "New_Dseq_Random_Result"
-)
-val put_new_dseq_result = New_Dseq_Result.put
+val get_pred_result = #1 o Data.get;
+val get_dseq_result = #2 o Data.get;
+val get_lseq_result = #3 o Data.get;
+val get_new_dseq_result = #4 o Data.get;
+val get_cps_result = #5 o Data.get;
-structure CPS_Result = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> (bool * term list) option
- fun init _ () = raise Fail "CPS_Result"
-)
-val put_cps_result = CPS_Result.put
+val put_pred_result = Data.map o @{apply 5(1)} o K;
+val put_dseq_result = Data.map o @{apply 5(2)} o K;
+val put_lseq_result = Data.map o @{apply 5(3)} o K;
+val put_new_dseq_result = Data.map o @{apply 5(4)} o K;
+val put_cps_result = Data.map o @{apply 5(5)} o K;
val target = "Quickcheck"
@@ -293,9 +285,11 @@
Pos_Random_DSeq =>
let
val compiled_term =
- Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+ Code_Runtime.dynamic_value_strict
+ (get_dseq_result, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
(Proof_Context.init_global thy4) (SOME target)
- (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
+ (fn proc => fn g => fn n => fn size => fn s =>
+ g n size s |>> (Limited_Sequence.map o map) proc)
qc_term []
in
(fn size => fn nrandom => fn depth =>
@@ -306,7 +300,7 @@
let
val compiled_term =
Code_Runtime.dynamic_value_strict
- (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
+ (get_lseq_result, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
(Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
@@ -322,18 +316,20 @@
let
val compiled_term =
Code_Runtime.dynamic_value_strict
- (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
+ (get_new_dseq_result, put_new_dseq_result,
+ "Predicate_Compile_Quickcheck.put_new_dseq_result")
(Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
qc_term []
in
- fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
+ fn size => fn nrandom => fn depth =>
+ Option.map fst (Lazy_Sequence.yield (compiled_term depth))
end
| Pos_Generator_CPS =>
let
val compiled_term =
Code_Runtime.dynamic_value_strict
- (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
+ (get_cps_result, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
(Proof_Context.init_global thy4) (SOME target)
(fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
qc_term []
@@ -343,8 +339,9 @@
| Depth_Limited_Random =>
let
val compiled_term = Code_Runtime.dynamic_value_strict
- (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
- (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+ (get_pred_result, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
+ (Proof_Context.init_global thy4) (SOME target)
+ (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
g depth nrandom size seed |> (Predicate.map o map) proc)
qc_term []
in
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Dec 19 20:10:59 2014 +0100
@@ -440,32 +440,30 @@
Bound 0 $ @{term "None :: term list option"} $ return)
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
+
(** generator compiliation **)
-(* FIXME just one data slot (record) per program unit *)
-
-structure Counterexample = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> bool ->
- Code_Numeral.natural -> (bool * term list) option
- fun init _ () = raise Fail "Counterexample"
-);
-val put_counterexample = Counterexample.put;
-
-structure Counterexample_Batch = Proof_Data
+structure Data = Proof_Data
(
- type T = unit -> (Code_Numeral.natural -> term list option) list
- fun init _ () = raise Fail "Counterexample"
+ type T =
+ (unit -> Code_Numeral.natural -> bool ->
+ Code_Numeral.natural -> (bool * term list) option) *
+ (unit -> (Code_Numeral.natural -> term list option) list) *
+ (unit -> (Code_Numeral.natural -> bool) list);
+ val empty: T =
+ (fn () => raise Fail "counterexample",
+ fn () => raise Fail "counterexample_batch",
+ fn () => raise Fail "validator_batch");
+ fun init _ = empty;
);
-val put_counterexample_batch = Counterexample_Batch.put;
-structure Validator_Batch = Proof_Data
-(
- type T = unit -> (Code_Numeral.natural -> bool) list
- fun init _ () = raise Fail "Counterexample"
-);
-val put_validator_batch = Validator_Batch.put;
+val get_counterexample = #1 o Data.get;
+val get_counterexample_batch = #2 o Data.get;
+val get_validator_batch = #3 o Data.get;
+val put_counterexample = Data.map o @{apply 3(1)} o K;
+val put_counterexample_batch = Data.map o @{apply 3(2)} o K;
+val put_validator_batch = Data.map o @{apply 3(3)} o K;
val target = "Quickcheck";
@@ -477,7 +475,7 @@
else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
+ (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
ctxt (SOME target) (fn proc => fn g =>
fn card => fn genuine_only => fn size => g card genuine_only size
|> (Option.map o apsnd o map) proc) t' []
@@ -498,7 +496,7 @@
let
val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
val compiles = Code_Runtime.dynamic_value_strict
- (Counterexample_Batch.get, put_counterexample_batch,
+ (get_counterexample_batch, put_counterexample_batch,
"Exhaustive_Generators.put_counterexample_batch")
ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
(HOLogic.mk_list @{typ "natural => term list option"} ts') []
@@ -516,7 +514,7 @@
val ts' = map (mk_validator_expr ctxt) ts
in
Code_Runtime.dynamic_value_strict
- (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
+ (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
end;
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Dec 19 20:10:59 2014 +0100
@@ -134,7 +134,7 @@
(U', Const (@{const_name Quickcheck_Narrowing.apply},
narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
end
-
+
fun mk_sum (t, u) =
let
val T = fastype_of t
@@ -171,7 +171,7 @@
in
eqs
end
-
+
fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
(case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
@@ -217,19 +217,19 @@
fun elapsed_time description e =
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
-
+
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
let
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
fun message s = if quiet then () else writeln s
fun verbose_message s = if not quiet andalso verbose then writeln s else ()
val current_size = Unsynchronized.ref 0
- val current_result = Unsynchronized.ref Quickcheck.empty_result
+ val current_result = Unsynchronized.ref Quickcheck.empty_result
val tmp_prefix = "Quickcheck_Narrowing"
val ghc_options = Config.get ctxt ghc_options
val with_tmp_dir =
- if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
- fun run in_path =
+ if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
+ fun run in_path =
let
fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
val generatedN = Code_Target.generatedN
@@ -282,7 +282,7 @@
^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
- |> Context.proof_map (exec false ml_code);
+ |> Context.proof_map (exec false ml_code);
val counterexample = get ctxt' ()
in
if is_genuine counterexample then
@@ -296,7 +296,7 @@
with_size true (k + 1))
end
end
- end
+ end
in with_size genuine_only 0 end
in
with_tmp_dir tmp_prefix run
@@ -309,44 +309,45 @@
(Code_Target.evaluator ctxt target program deps true vs_ty_t);
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
+
(** counterexample generator **)
-(* FIXME just one data slot (record) per program unit *)
-structure Counterexample = Proof_Data
-(
- type T = unit -> (bool * term list) option
- fun init _ () = raise Fail "Counterexample"
-)
-
-datatype counterexample = Universal_Counterexample of (term * counterexample)
+datatype counterexample =
+ Universal_Counterexample of (term * counterexample)
| Existential_Counterexample of (term * counterexample) list
| Empty_Assignment
-
+
fun map_counterexample f Empty_Assignment = Empty_Assignment
| map_counterexample f (Universal_Counterexample (t, c)) =
Universal_Counterexample (f t, map_counterexample f c)
| map_counterexample f (Existential_Counterexample cs) =
Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
-(* FIXME just one data slot (record) per program unit *)
-structure Existential_Counterexample = Proof_Data
+structure Data = Proof_Data
(
- type T = unit -> counterexample option
- fun init _ () = raise Fail "Counterexample"
-)
+ type T =
+ (unit -> (bool * term list) option) *
+ (unit -> counterexample option);
+ val empty: T =
+ (fn () => raise Fail "counterexample",
+ fn () => raise Fail "existential_counterexample");
+ fun init _ = empty;
+);
-val put_existential_counterexample = Existential_Counterexample.put
+val get_counterexample = #1 o Data.get;
+val get_existential_counterexample = #2 o Data.get;
-val put_counterexample = Counterexample.put
+val put_counterexample = Data.map o @{apply 2(1)} o K;
+val put_existential_counterexample = Data.map o @{apply 2(2)} o K;
fun finitize_functions (xTs, t) =
let
val (names, boundTs) = split_list xTs
fun mk_eval_ffun dT rT =
- Const (@{const_name "Quickcheck_Narrowing.eval_ffun"},
+ Const (@{const_name "Quickcheck_Narrowing.eval_ffun"},
Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
fun mk_eval_cfun dT rT =
- Const (@{const_name "Quickcheck_Narrowing.eval_cfun"},
+ Const (@{const_name "Quickcheck_Narrowing.eval_cfun"},
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
fun eval_function (Type (@{type_name fun}, [dT, rT])) =
let
@@ -437,10 +438,10 @@
map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
|> map (apsnd post_process)
end
-
+
fun test_term ctxt catch_code_errors (t, _) =
let
- fun dest_result (Quickcheck.Result r) = r
+ fun dest_result (Quickcheck.Result r) = r
val opts =
((Config.get ctxt Quickcheck.genuine_only,
(Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
@@ -457,12 +458,14 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
val act = if catch_code_errors then try else (fn f => SOME o f)
- val execute = dynamic_value_strict (true, opts)
- ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
- "Narrowing_Generators.put_existential_counterexample"))
- ctxt (apfst o Option.map o map_counterexample)
- in
- case act execute (mk_property qs prop_t) of
+ val execute =
+ dynamic_value_strict (true, opts)
+ ((K true, fn _ => error ""),
+ (get_existential_counterexample, put_existential_counterexample,
+ "Narrowing_Generators.put_existential_counterexample"))
+ ctxt (apfst o Option.map o map_counterexample)
+ in
+ case act execute (mk_property qs prop_t) of
SOME (counterexample, result) => Quickcheck.Result
{counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
evaluation_terms = Option.map (K []) counterexample,
@@ -479,16 +482,18 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
- fun is_genuine (SOME (true, _)) = true
+ fun is_genuine (SOME (true, _)) = true
| is_genuine _ = false
val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
val act = if catch_code_errors then try else (fn f => SOME o f)
- val execute = dynamic_value_strict (false, opts)
- ((is_genuine, counterexample_of),
- (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
- ctxt (apfst o Option.map o apsnd o map)
+ val execute =
+ dynamic_value_strict (false, opts)
+ ((is_genuine, counterexample_of),
+ (get_counterexample, put_counterexample,
+ "Narrowing_Generators.put_counterexample"))
+ ctxt (apfst o Option.map o apsnd o map)
in
- case act execute (ensure_testable (finitize t')) of
+ case act execute (ensure_testable (finitize t')) of
SOME (counterexample, result) =>
Quickcheck.Result
{counterexample = counterexample_of counterexample,
@@ -528,5 +533,5 @@
#> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
(@{sort narrowing}, instantiate_narrowing_datatype)
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
-
+
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Dec 19 20:10:59 2014 +0100
@@ -266,23 +266,27 @@
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
+
(** building and compiling generator expressions **)
-(* FIXME just one data slot (record) per program unit *)
-
-structure Counterexample = Proof_Data
+structure Data = Proof_Data
(
- type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed
- fun init _ () = raise Fail "Counterexample"
+ type T =
+ (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed ->
+ (bool * term list) option * seed) *
+ (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed ->
+ ((bool * term list) option * (bool list * bool)) * seed);
+ val empty: T =
+ (fn () => raise Fail "counterexample",
+ fn () => raise Fail "counterexample_report");
+ fun init _ = empty;
);
-val put_counterexample = Counterexample.put;
-structure Counterexample_Report = Proof_Data
-(
- type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed
- fun init _ () = raise Fail "Counterexample_Report"
-);
-val put_counterexample_report = Counterexample_Report.put;
+val get_counterexample = #1 o Data.get;
+val get_counterexample_report = #2 o Data.get;
+
+val put_counterexample = Data.map o @{apply 2(1)} o K;
+val put_counterexample_report = Data.map o @{apply 2(2)} o K;
val target = "Quickcheck";
@@ -407,11 +411,14 @@
if Config.get ctxt Quickcheck.report then
let
val t' = mk_parametric_reporting_generator_expr ctxt ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
- ctxt (SOME target)
- (fn proc => fn g => fn c => fn b => fn s => g c b s
- #>> (apfst o Option.map o apsnd o map) proc) t' [];
+ val compile =
+ Code_Runtime.dynamic_value_strict
+ (get_counterexample_report, put_counterexample_report,
+ "Random_Generators.put_counterexample_report")
+ ctxt (SOME target)
+ (fn proc => fn g => fn c => fn b => fn s =>
+ g c b s #>> (apfst o Option.map o apsnd o map) proc)
+ t' [];
fun single_tester c b s = compile c b s |> Random_Engine.run
fun iterate_and_collect _ _ 0 report = (NONE, report)
| iterate_and_collect genuine_only (card, size) j report =
@@ -429,11 +436,13 @@
else
let
val t' = mk_parametric_generator_expr ctxt ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
- ctxt (SOME target)
- (fn proc => fn g => fn c => fn b => fn s => g c b s
- #>> (Option.map o apsnd o map) proc) t' [];
+ val compile =
+ Code_Runtime.dynamic_value_strict
+ (get_counterexample, put_counterexample, "Random_Generators.put_counterexample")
+ ctxt (SOME target)
+ (fn proc => fn g => fn c => fn b => fn s =>
+ g c b s #>> (Option.map o apsnd o map) proc)
+ t' [];
fun single_tester c b s = compile c b s |> Random_Engine.run
fun iterate _ _ 0 = NONE
| iterate genuine_only (card, size) j =