src/Tools/quickcheck.ML
changeset 46477 db693eb03a3f
parent 46343 6d9535e52915
child 46565 ad21900e0ee9
equal deleted inserted replaced
46457:915af80f74b3 46477:db693eb03a3f
    19   val depth : int Config.T
    19   val depth : int Config.T
    20   val no_assms : bool Config.T
    20   val no_assms : bool Config.T
    21   val report : bool Config.T
    21   val report : bool Config.T
    22   val timing : bool Config.T
    22   val timing : bool Config.T
    23   val genuine_only : bool Config.T
    23   val genuine_only : bool Config.T
       
    24   val abort_potential : bool Config.T  
    24   val quiet : bool Config.T
    25   val quiet : bool Config.T
    25   val verbose : bool Config.T
    26   val verbose : bool Config.T
    26   val timeout : real Config.T
    27   val timeout : real Config.T
    27   val allow_function_inversion : bool Config.T;
    28   val allow_function_inversion : bool Config.T;
    28   val finite_types : bool Config.T
    29   val finite_types : bool Config.T
   175 
   176 
   176 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
   177 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
   177 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
   178 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
   178 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
   179 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
   179 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
   180 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
       
   181 val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
   180 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
   182 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
   181 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
   183 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
   182 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
   184 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
   183 val allow_function_inversion =
   185 val allow_function_inversion =
   184   Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
   186   Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
   431       ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
   433       ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
   432   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   434   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   433   | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
   435   | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
   434   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
   436   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
   435   | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
   437   | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
       
   438   | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
   436   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   439   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   437   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   440   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   438   | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
   441   | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
   439   | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
   442   | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
   440   | parse_test_param ("allow_function_inversion", [arg]) =
   443   | parse_test_param ("allow_function_inversion", [arg]) =