--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue May 31 17:15:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue May 31 18:13:00 2011 +0200
@@ -6,8 +6,7 @@
signature NARROWING_GENERATORS =
sig
- val compile_generator_expr:
- Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+ val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
val finite_functions : bool Config.T
val overlord : bool Config.T
@@ -197,8 +196,9 @@
val _ = Isabelle_System.mkdirs path;
in Exn.release (Exn.capture f path) end;
-fun value ctxt (get, put, put_ml) (code, value) size =
+fun value ctxt (get, put, put_ml) (code, value_name) =
let
+ fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
val tmp_prefix = "Quickcheck_Narrowing"
val with_tmp_dir =
if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
@@ -208,45 +208,55 @@
val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
val main_file = Path.append in_path (Path.basic "Main.hs")
val main = "module Main where {\n\n" ^
+ "import System;\n" ^
"import Narrowing_Engine;\n" ^
"import Code;\n\n" ^
- "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
+ "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
"}\n"
val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
(unprefix "module Code where {" code)
val _ = File.write code_file code'
val _ = File.write narrowing_engine_file narrowing_engine
val _ = File.write main_file main
- val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
- val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
+ val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+ val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
- " -o " ^ executable ^ "; ) && " ^ executable
- in
- bash_output cmd
+ " -o " ^ executable ^ ";"
+ val _ = if bash cmd <> 0 then
+ error "Compilation failed!"
+ else
+ ()
+ fun with_size k =
+ if k > Config.get ctxt Quickcheck.size then
+ NONE
+ else
+ let
+ val _ = message ("Test data size: " ^ string_of_int k)
+ val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
+ in
+ if response = "NONE\n" then with_size (k + 1) else SOME response
+ end
+ in case with_size 0 of
+ NONE => NONE
+ | SOME response =>
+ let
+ val output_value = the_default "NONE"
+ (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
+ |> translate_string (fn s => if s = "\\" then "\\\\" else s)
+ val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+ ^ " (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);
+ in get ctxt' () end
end
- val result = with_tmp_dir tmp_prefix run
- val output_value = the_default "NONE"
- (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
- |> translate_string (fn s => if s = "\\" then "\\\\" else s)
- val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
- ^ " (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);
- in get ctxt' () end;
+ in with_tmp_dir tmp_prefix run end;
-fun evaluation cookie thy evaluator vs_t args size =
+fun dynamic_value_strict cookie thy postproc t =
let
- val ctxt = Proof_Context.init_global thy;
- val (program_code, value_name) = evaluator vs_t;
- val value_code = space_implode " "
- (value_name :: "()" :: map (enclose "(" ")") args);
- in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
-
-fun dynamic_value_strict cookie thy postproc t args size =
- let
- fun evaluator naming program ((_, vs_ty), t) deps =
- evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
+ val ctxt = Proof_Context.init_global thy
+ fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value ctxt cookie)
+ (Code_Target.evaluator thy target naming program deps (vs_ty, t));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
@@ -286,7 +296,9 @@
list_abs (names ~~ Ts', t'')
end
-fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
+(** tester **)
+
+fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
val t' = list_abs_free (Term.add_frees t [], t)
@@ -295,11 +307,22 @@
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
val result = dynamic_value_strict
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
- thy (Option.map o map) (ensure_testable t'') [] size
+ thy (Option.map o map) (ensure_testable t'')
in
- (result, NONE)
+ Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
+ evaluation_terms = Option.map (K []) result, timings = [], reports = []}
end;
+fun test_goals ctxt (limit_time, is_interactive) insts goals =
+ let
+ val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
+ in
+ if Config.get ctxt Quickcheck.finite_types then
+ error "Quickcheck-Narrowing does not support finite_types"
+ else
+ Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+ end
+
(* setup *)
val setup =
@@ -307,7 +330,6 @@
#> Code.datatype_interpretation ensure_partial_term_of_code
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
- #> Context.theory_map
- (Quickcheck.add_generator ("narrowing", compile_generator_expr))
+ #> Context.theory_map (Quickcheck.add_tester ("narrowing", test_goals))
end;
\ No newline at end of file
--- a/src/Tools/quickcheck.ML Tue May 31 17:15:14 2011 +0200
+++ b/src/Tools/quickcheck.ML Tue May 31 18:13:00 2011 +0200
@@ -31,16 +31,6 @@
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
- (* registering generators *)
- val add_generator:
- string * (Proof.context -> (term * term list) list -> int list -> 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
- val add_batch_validator:
- string * (Proof.context -> term list -> (int -> bool) list)
- -> Context.generic -> Context.generic
(* quickcheck's result *)
datatype result =
Result of
@@ -50,6 +40,23 @@
reports : (int * report) list}
val counterexample_of : result -> (string * term) list option
val timings_of : result -> (string * int) list
+ (* registering generators *)
+ val add_generator:
+ string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
+ -> Context.generic -> Context.generic
+ val add_tester:
+ string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)
+ -> Context.generic -> Context.generic
+ val add_batch_generator:
+ string * (Proof.context -> term list -> (int -> term list option) list)
+ -> Context.generic -> Context.generic
+ val add_batch_validator:
+ string * (Proof.context -> term list -> (int -> bool) list)
+ -> Context.generic -> Context.generic
+ (* basic operations *)
+ val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
+ -> (typ option * (term * term list)) list list
+ val collect_results: ('a -> result) -> 'a list -> result list -> result list
(* testing terms and proof states *)
val test_term: Proof.context -> bool * bool -> term * term list -> result
val test_goal_terms:
@@ -174,17 +181,19 @@
structure Data = Generic_Data
(
type T =
- ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+ (((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
+ * (string * (Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list)) list)
* ((string * (Proof.context -> term list -> (int -> term list option) list)) list
* ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
* test_params;
- val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
+ val empty = ((([], []), ([], [])), Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
- fun merge (((generators1, (batch_generators1, batch_validators1)), params1),
- ((generators2, (batch_generators2, batch_validators2)), params2)) : T =
- ((AList.merge (op =) (K true) (generators1, generators2),
- (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
- AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
+ fun merge ((((generators1, testers1), (batch_generators1, batch_validators1)), params1),
+ (((generators2, testers2), (batch_generators2, batch_validators2)), params2)) : T =
+ (((AList.merge (op =) (K true) (generators1, generators2),
+ AList.merge (op =) (K true) (testers1, testers2)),
+ (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
+ AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
merge_test_params (params1, params2));
);
@@ -196,7 +205,9 @@
val map_test_params = Data.map o apsnd o map_test_params'
-val add_generator = Data.map o apfst o apfst o AList.update (op =);
+val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);
+
+val add_tester = Data.map o apfst o apfst o apsnd o AList.update (op =);
val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
@@ -223,12 +234,15 @@
end
val mk_tester =
- gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt))
+ gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
val mk_batch_tester =
gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
val mk_batch_validator =
gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
+
+fun lookup_tester ctxt = AList.lookup (op =) ((snd o fst o fst o Data.get o Context.Proof) ctxt)
+
(* testing propositions *)
fun check_test_term t =
@@ -403,7 +417,7 @@
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
-fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
+fun instantiate_goals lthy insts goals =
let
fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
val thy = Proof_Context.theory_of lthy
@@ -417,7 +431,7 @@
(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, eval_terms))]) check_goals
+ [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
val error_msg =
cat_lines
(maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
@@ -428,20 +442,28 @@
[[]] => error error_msg
| xs => xs
val _ = if Config.get lthy quiet then () else warning error_msg
- fun collect_results f [] results = results
- | collect_results f (t :: ts) results =
- let
- val result = f t
- in
- if found_counterexample result then
- (result :: results)
- else
- collect_results f ts (result :: results)
- end
+ in
+ correct_inst_goals
+ end
+
+fun collect_results f [] results = results
+ | collect_results f (t :: ts) results =
+ let
+ val result = f t
+ in
+ if found_counterexample result then
+ (result :: results)
+ else
+ collect_results f ts (result :: results)
+ end
+
+fun test_goal_terms lthy (limit_time, is_interactive) insts goals =
+ let
fun test_term' goal =
case goal of
[(NONE, t)] => test_term lthy (limit_time, is_interactive) t
| ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
+ val correct_inst_goals = instantiate_goals lthy insts goals
in
if Config.get lthy finite_types then
collect_results test_term' correct_inst_goals []
@@ -465,13 +487,14 @@
of NONE => Assumption.all_assms_of lthy
| 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
+ val goals = case some_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);
+ val test_goals = the_default test_goal_terms (lookup_tester lthy (Config.get lthy tester))
in
- test_goal_terms lthy (time_limit, is_interactive) insts check_goals
+ test_goals lthy (time_limit, is_interactive) insts goals
end
(* pretty printing *)
@@ -544,7 +567,9 @@
| read_expectation "counterexample" = Counterexample
| read_expectation s = error ("Not an expectation value: " ^ s)
-fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt)))
+fun valid_tester_name genctxt name =
+ AList.defined (op =) (fst (fst (fst (Data.get genctxt)))) name orelse
+ AList.defined (op =) (snd (fst (fst (Data.get genctxt)))) name
fun parse_tester name genctxt =
if valid_tester_name genctxt name then