# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 1108529100cea92f733f47a411dc12d1ffabdf89
# Parent  7febf76e0a69f7f55b43fee86f9a7fedc312f123
checking if parameter is name of a tester which allows e.g. quickcheck[random]

diff -r 7febf76e0a69 -r 1108529100ce src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -342,7 +342,15 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)  
 
-fun parse_test_param ("tester", [arg]) = Config.put_generic tester arg
+fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt))
+
+fun parse_tester name genctxt =
+  if valid_tester_name genctxt name then
+    Config.put_generic tester name genctxt
+  else
+    error ("Unknown tester: " ^ name)
+
+fun parse_test_param ("tester", [arg]) = parse_tester arg
   | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
   | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
   | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
@@ -354,7 +362,10 @@
   | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
   | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
   | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
-  | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
+  | parse_test_param (name, _) = fn genctxt =>
+    if valid_tester_name genctxt name then
+      Config.put_generic tester name genctxt
+    else error ("Unknown tester or test parameter: " ^ name);
 
 fun parse_test_param_inst (name, arg) (insts, ctxt) =
       case try (ProofContext.read_typ ctxt) name