src/Tools/quickcheck.ML
author bulwahn
Fri, 18 Mar 2011 18:19:42 +0100
changeset 42025 cb5b1e85b32e
parent 41862 a38536bf2736
child 42026 da9b58f1db42
permissions -rw-r--r--
adding eval option to quickcheck
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30824
bc6b24882834 fixed header;
wenzelm
parents: 30473
diff changeset
     1
(*  Title:      Tools/quickcheck.ML
40246
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
     2
    Author:     Stefan Berghofer, Florian Haftmann, Lukas Bulwahn, TU Muenchen
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     3
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     4
Generic counterexample search engine.
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     5
*)
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     6
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     7
signature QUICKCHECK =
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
     8
sig
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
     9
  val setup: theory -> theory
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    10
  (* configuration *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32297
diff changeset
    11
  val auto: bool Unsynchronized.ref
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34128
diff changeset
    12
  val timing : bool Unsynchronized.ref
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    13
  val tester : string Config.T
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    14
  val size : int Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    15
  val iterations : int Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    16
  val no_assms : bool Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    17
  val report : bool Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    18
  val quiet : bool Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    19
  val timeout : real Config.T
40648
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
    20
  val finite_types : bool Config.T
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
    21
  val finite_type_size : int Config.T
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    22
  datatype report = Report of
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    23
    { iterations : int, raised_match_errors : int,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    24
      satisfied_assms : int list, positive_concl_tests : int }
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    25
  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    26
  datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
40246
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
    27
  val test_params_of : Proof.context -> test_params
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    28
  val map_test_params : (typ list * expectation -> typ list * expectation)
40246
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
    29
    -> Context.generic -> Context.generic
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    30
  val add_generator:
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
    31
    string * (Proof.context -> term -> int -> term list option * report option)
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 39138
diff changeset
    32
      -> Context.generic -> Context.generic
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
    33
  val add_batch_generator:
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
    34
    string * (Proof.context -> term list -> (int -> term list option) list)
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
    35
      -> Context.generic -> Context.generic
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    36
  (* testing terms and proof states *)
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
    37
  val test_term: Proof.context -> bool * bool -> term ->
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
    38
    (string * term) list option * ((string * int) list * ((int * report) list) option)
40648
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
    39
  val test_goal_terms:
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
    40
    Proof.context -> bool * bool -> (string * typ) list -> term list
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
    41
      -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
37909
583543ad6ad1 changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents: 36960
diff changeset
    42
  val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
    43
  (* testing a batch of terms *)
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
    44
  val test_terms: Proof.context -> term list -> (string * term) list option list option
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    45
end;
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    46
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    47
structure Quickcheck : QUICKCHECK =
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    48
struct
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    49
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    50
(* preferences *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    51
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32297
diff changeset
    52
val auto = Unsynchronized.ref false;
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    53
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34128
diff changeset
    54
val timing = Unsynchronized.ref false;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34128
diff changeset
    55
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    56
val _ =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    57
  ProofGeneralPgip.add_preference Preferences.category_tracing
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39329
diff changeset
    58
  (Unsynchronized.setmp auto true (fn () =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    59
    Preferences.bool_pref auto
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    60
      "auto-quickcheck"
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39324
diff changeset
    61
      "Run Quickcheck automatically.") ());
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    62
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    63
(* quickcheck report *)
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    64
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    65
datatype report = Report of
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    66
  { iterations : int, raised_match_errors : int,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    67
    satisfied_assms : int list, positive_concl_tests : int }
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    68
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    69
(* expectation *)
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    70
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    71
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    72
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    73
fun merge_expectation (expect1, expect2) =
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    74
  if expect1 = expect2 then expect1 else No_Expectation
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
    75
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
    76
(* quickcheck configuration -- default parameters, test generators *)
40908
e8806880819e adding configuration quickcheck_tester
bulwahn
parents: 40906
diff changeset
    77
val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    78
val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    79
val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    80
val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    81
val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    82
val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    83
val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
40646
3dfa41e89738 adding option finite_types to quickcheck
bulwahn
parents: 40644
diff changeset
    84
val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    85
val (finite_type_size, setup_finite_type_size) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    86
  Attrib.config_int "quickcheck_finite_type_size" (K 3)
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
    87
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    88
val setup_config =
40908
e8806880819e adding configuration quickcheck_tester
bulwahn
parents: 40906
diff changeset
    89
  setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet
e8806880819e adding configuration quickcheck_tester
bulwahn
parents: 40906
diff changeset
    90
    #> setup_timeout #> setup_finite_types #> setup_finite_type_size
40646
3dfa41e89738 adding option finite_types to quickcheck
bulwahn
parents: 40644
diff changeset
    91
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    92
datatype test_params = Test_Params of
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    93
  {default_type: typ list, expect : expectation};
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
    94
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    95
fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    96
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    97
fun make_test_params (default_type, expect) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    98
  Test_Params {default_type = default_type, expect = expect};
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    99
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   100
fun map_test_params' f (Test_Params {default_type, expect}) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   101
  make_test_params (f (default_type, expect));
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   102
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   103
fun merge_test_params
41472
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41086
diff changeset
   104
  (Test_Params {default_type = default_type1, expect = expect1},
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41086
diff changeset
   105
    Test_Params {default_type = default_type2, expect = expect2}) =
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41086
diff changeset
   106
  make_test_params
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41086
diff changeset
   107
    (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   108
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 39138
diff changeset
   109
structure Data = Generic_Data
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33291
diff changeset
   110
(
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   111
  type T =
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   112
    ((string * (Proof.context -> term -> int -> term list option * report option)) list
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   113
      * (string * (Proof.context -> term list -> (int -> term list option) list)) list)
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   114
      * test_params;
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   115
  val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   116
  val extend = I;
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   117
  fun merge (((generators1, batch_generators1), params1), ((generators2, batch_generators2), params2)) : T =
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   118
    ((AList.merge (op =) (K true) (generators1, generators2),
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   119
    AList.merge (op =) (K true) (batch_generators1, batch_generators2)),
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   120
      merge_test_params (params1, params2));
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33291
diff changeset
   121
);
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   122
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 39138
diff changeset
   123
val test_params_of = snd o Data.get o Context.Proof;
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
   124
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   125
val default_type = fst o dest_test_params o test_params_of
40246
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
   126
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   127
val expect = snd o dest_test_params o test_params_of
40246
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
   128
c03fc7d3fa97 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
bulwahn
parents: 40225
diff changeset
   129
val map_test_params = Data.map o apsnd o map_test_params'
39253
0c47d615a69b removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents: 39252
diff changeset
   130
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   131
val add_generator = Data.map o apfst o apfst o AList.update (op =);
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   132
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   133
val add_batch_generator = Data.map o apfst o apsnd o AList.update (op =);
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   134
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   135
(* generating tests *)
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   136
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   137
fun gen_mk_tester lookup ctxt v =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   138
  let
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   139
    val name = Config.get ctxt tester
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   140
    val tester = case lookup ctxt name
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   141
      of NONE => error ("No such quickcheck tester: " ^ name)
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   142
      | SOME tester => tester ctxt;
40235
87998864284e use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents: 40225
diff changeset
   143
  in
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   144
    if Config.get ctxt quiet then
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   145
      try tester v
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   146
    else
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   147
      let
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   148
        val tester = Exn.interruptible_capture tester v
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   149
      in case Exn.get_result tester of
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   150
          NONE => SOME (Exn.release tester)
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   151
        | SOME tester => SOME tester
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   152
      end
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   153
  end
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   154
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   155
val mk_tester = gen_mk_tester (fn ctxt =>
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   156
  AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt))
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   157
val mk_batch_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o fst o Data.get o Context.Proof) ctxt))
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   158
  
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   159
(* testing propositions *)
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   160
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   161
fun prep_test_term t =
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   162
  let
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28952
diff changeset
   163
    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   164
      error "Term to be tested contains type variables";
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28952
diff changeset
   165
    val _ = null (Term.add_vars t []) orelse
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   166
      error "Term to be tested contains schematic variables";
31138
a51ce445d498 dropped legacy operations
haftmann
parents: 30980
diff changeset
   167
    val frees = Term.add_frees t [];
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   168
  in (frees, list_abs_free (frees, t)) end
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   169
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   170
fun cpu_time description f =
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   171
  let
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   172
    val start = start_timing ()
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   173
    val result = Exn.capture f ()
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   174
    val time = Time.toMilliseconds (#cpu (end_timing start))
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35077
diff changeset
   175
  in (Exn.release result, (description, time)) end
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   176
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   177
fun limit ctxt (limit_time, is_interactive) f exc () =
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   178
  if limit_time then
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   179
      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f ()
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   180
    handle TimeLimit.TimeOut =>
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   181
      if is_interactive then exc () else raise TimeLimit.TimeOut
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   182
  else
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   183
    f ()
41753
dbd00d8a4784 quickcheck invokes TimeLimit.timeLimit only in one separate function
bulwahn
parents: 41735
diff changeset
   184
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   185
fun test_term ctxt (limit_time, is_interactive) t =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   186
  let
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   187
    val (names, t') = apfst (map fst) (prep_test_term t);
40366
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   188
    val current_size = Unsynchronized.ref 0
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   189
    fun excipit s =
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   190
      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   191
    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   192
    fun with_size test_fun k reports =
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   193
      if k > Config.get ctxt size then
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   194
        (NONE, reports)
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   195
      else
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   196
        let
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   197
          val _ = if Config.get ctxt quiet then () else Output.urgent_message
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   198
            ("Test data size: " ^ string_of_int k)
40648
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   199
          val _ = current_size := k
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   200
          val ((result, new_report), timing) =
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   201
            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   202
          val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   203
        in
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   204
          case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports)
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   205
        end;
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34128
diff changeset
   206
  in
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   207
    case test_fun of NONE => (NONE, ([comp_time], NONE))
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   208
      | SOME test_fun =>
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   209
        limit ctxt (limit_time, is_interactive) (fn () =>
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   210
          let
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   211
            val ((result, reports), exec_time) =
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   212
              cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   213
          in
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   214
            (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
40916
9928083506b6 improving presentation of quickcheck reports
bulwahn
parents: 40912
diff changeset
   215
              ([exec_time, comp_time],
9928083506b6 improving presentation of quickcheck reports
bulwahn
parents: 40912
diff changeset
   216
               if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
41753
dbd00d8a4784 quickcheck invokes TimeLimit.timeLimit only in one separate function
bulwahn
parents: 41735
diff changeset
   217
          end) (fn () => error (excipit "ran out of time")) ()
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   218
  end;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   219
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   220
fun test_terms ctxt ts =
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   221
  let
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   222
    val (namess, ts') = split_list (map (fn t => apfst (map fst) (prep_test_term t)) ts)
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   223
    val test_funs = mk_batch_tester ctxt ts'
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   224
    fun with_size tester k =
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   225
      if k > Config.get ctxt size then NONE
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   226
      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   227
    val results =
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   228
      Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   229
            (fn () => with_size test_fun 1)  ()
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   230
           handle TimeLimit.TimeOut => NONE)) test_funs
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   231
  in
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   232
    Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   233
  end
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   234
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   235
(* FIXME: this function shows that many assumptions are made upon the generation *)
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   236
(* In the end there is probably no generic quickcheck interface left... *)
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   237
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   238
fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   239
  let
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   240
    val thy = ProofContext.theory_of ctxt
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   241
    val (freess, ts') = split_list (map prep_test_term ts)
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   242
    val Ts = map snd (hd freess)
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   243
    val (test_funs, comp_time) = cpu_time "quickcheck compilation"
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   244
      (fn () => map (mk_tester ctxt) ts')
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   245
    fun test_card_size (card, size) =
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   246
      (* FIXME: why decrement size by one? *)
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   247
      case fst (the (nth test_funs (card - 1)) (size - 1)) of
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   248
        SOME ts => SOME (map fst (nth freess (card - 1)) ~~ ts)
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   249
      | NONE => NONE
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   250
    val enumeration_card_size =
41086
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   251
      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   252
        (* size does not matter *)
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   253
        map (rpair 0) (1 upto (length ts))
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   254
      else
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   255
        (* size does matter *)
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   256
        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
b4cccce25d9a if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn
parents: 41043
diff changeset
   257
        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   258
    in
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   259
      if (forall is_none test_funs) then
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   260
        (NONE, ([comp_time], NONE))
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   261
      else if (forall is_some test_funs) then
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   262
        limit ctxt (limit_time, is_interactive) (fn () =>
41753
dbd00d8a4784 quickcheck invokes TimeLimit.timeLimit only in one separate function
bulwahn
parents: 41735
diff changeset
   263
          (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
dbd00d8a4784 quickcheck invokes TimeLimit.timeLimit only in one separate function
bulwahn
parents: 41735
diff changeset
   264
          (fn () => error "Quickcheck ran out of time") ()
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   265
      else
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   266
        error "Unexpectedly, testers of some cardinalities are executable but others are not"
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   267
    end
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   268
40647
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   269
fun get_finite_types ctxt =
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   270
  fst (chop (Config.get ctxt finite_type_size)
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   271
    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   272
     "Enum.finite_4", "Enum.finite_5"]))
40647
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   273
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   274
exception WELLSORTED of string
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   275
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   276
fun monomorphic_term thy insts default_T =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   277
  let
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   278
    fun subst (T as TFree (v, S)) =
40903
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   279
      let
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   280
        val T' = AList.lookup (op =) insts v
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   281
          |> the_default default_T
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   282
      in if Sign.of_sort thy (T', S) then T'
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   283
        else raise (WELLSORTED ("For instantiation with default_type " ^
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   284
          Syntax.string_of_typ_global thy default_T ^
40903
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   285
          ":\n" ^ Syntax.string_of_typ_global thy T' ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   286
          " to be substituted for variable " ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   287
          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   288
          Syntax.string_of_sort_global thy S))
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   289
      end
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   290
      | subst T = T;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   291
  in (map_types o map_atyps) subst end;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   292
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   293
datatype wellsorted_error = Wellsorted_Error of string | Term of term
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   294
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   295
fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   296
  let
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   297
    val thy = ProofContext.theory_of lthy
40926
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   298
    val default_insts =
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   299
      if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
40647
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   300
    val inst_goals =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   301
      map (fn check_goal =>
40926
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   302
        if not (null (Term.add_tfree_names check_goal [])) then
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   303
          map (fn T =>
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   304
            (pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T)
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   305
              check_goal
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   306
              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
40926
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   307
        else
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   308
          [(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   309
    val error_msg =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   310
      cat_lines
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   311
        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   312
    fun is_wellsorted_term (T, Term t) = SOME (T, t)
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   313
      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   314
    val correct_inst_goals =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   315
      case map (map_filter is_wellsorted_term) inst_goals of
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   316
        [[]] => error error_msg
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   317
      | xs => xs
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   318
    val _ = if Config.get lthy quiet then () else warning error_msg
37912
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   319
    fun collect_results f reports [] = (NONE, rev reports)
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   320
      | collect_results f reports (t :: ts) =
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   321
        case f t of
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   322
          (SOME res, report) => (SOME res, rev (report :: reports))
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   323
        | (NONE, report) => collect_results f (report :: reports) ts
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   324
    fun test_term' goal =
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   325
      case goal of
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   326
        [(NONE, t)] => test_term lthy (limit_time, is_interactive) t
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   327
      | ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   328
  in
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   329
    if Config.get lthy finite_types then
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   330
      collect_results test_term' [] correct_inst_goals
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   331
    else
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   332
      collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals)
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   333
  end;
37912
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   334
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   335
fun test_goal (time_limit, is_interactive) insts i state =
40648
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   336
  let
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   337
    val lthy = Proof.context_of state;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   338
    val thy = Proof.theory_of state;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   339
    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   340
      | strip t = t;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   341
    val {goal = st, ...} = Proof.raw_goal state;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   342
    val (gi, frees) = Logic.goal_params (prop_of st) i;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   343
    val some_locale = case (Option.map #target o Named_Target.peek) lthy
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   344
     of NONE => NONE
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   345
      | SOME "" => NONE
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   346
      | SOME locale => SOME locale;
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   347
    val assms = if Config.get lthy no_assms then [] else case some_locale
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   348
     of NONE => Assumption.all_assms_of lthy
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   349
      | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   350
    val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   351
    val check_goals = case some_locale
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   352
     of NONE => [proto_goal]
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   353
      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   354
        (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   355
  in
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   356
    test_goal_terms lthy (time_limit, is_interactive) insts check_goals
40648
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   357
  end
1598ec648b0d splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck
bulwahn
parents: 40647
diff changeset
   358
37912
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   359
(* pretty printing *)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   360
40225
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   361
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   362
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   363
fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   364
  | pretty_counterex ctxt auto (SOME cex) =
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   365
      Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   366
        map (fn (s, t) =>
40916
9928083506b6 improving presentation of quickcheck reports
bulwahn
parents: 40912
diff changeset
   367
          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex));
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   368
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   369
fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   370
    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   371
  let
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   372
    fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)])
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   373
  in
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   374
     ([pretty_stat "iterations" iterations,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   375
     pretty_stat "match exceptions" raised_match_errors]
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   376
     @ map_index
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   377
       (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n)
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   378
       satisfied_assms
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   379
     @ [pretty_stat "positive conclusion tests" positive_concl_tests])
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   380
  end
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   381
35380
6ac5b81a763d adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents: 35379
diff changeset
   382
fun pretty_reports ctxt (SOME reports) =
40916
9928083506b6 improving presentation of quickcheck reports
bulwahn
parents: 40912
diff changeset
   383
  Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   384
    maps (fn (size, report) =>
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   385
      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   386
      (rev reports))
35380
6ac5b81a763d adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents: 35379
diff changeset
   387
  | pretty_reports ctxt NONE = Pretty.str ""
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   388
40225
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   389
fun pretty_counterex_and_reports ctxt auto (cex, timing_and_reports) =
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   390
  Pretty.chunks (pretty_counterex ctxt auto cex ::
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   391
    map (pretty_reports ctxt) (map snd timing_and_reports))
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   392
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   393
(* automatic testing *)
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   394
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 33560
diff changeset
   395
fun auto_quickcheck state =
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   396
  let
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   397
    val ctxt = Proof.context_of state;
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   398
    val res =
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   399
      state
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   400
      |> Proof.map_context (Config.put report false #> Config.put quiet true)
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   401
      |> try (test_goal (false, false) [] 1);
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   402
  in
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   403
    case res of
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   404
      NONE => (false, state)
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   405
    | SOME (NONE, report) => (false, state)
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   406
    | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   407
        Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   408
  end
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 33560
diff changeset
   409
40931
061b8257ab9f run synchronous Auto Tools in parallel
blanchet
parents: 40926
diff changeset
   410
val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   411
  #> setup_config
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   412
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
   413
(* Isar commands *)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   414
28336
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   415
fun read_nat s = case (Library.read_int o Symbol.explode) s
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   416
 of (k, []) => if k >= 0 then k
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   417
      else error ("Not a natural number: " ^ s)
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   418
  | (_, _ :: _) => error ("Not a natural number: " ^ s);
37909
583543ad6ad1 changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
bulwahn
parents: 36960
diff changeset
   419
34128
8650a073dd9b made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents: 33583
diff changeset
   420
fun read_bool "false" = false
8650a073dd9b made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents: 33583
diff changeset
   421
  | read_bool "true" = true
8650a073dd9b made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents: 33583
diff changeset
   422
  | read_bool s = error ("Not a Boolean value: " ^ s)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   423
40366
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   424
fun read_real s =
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   425
  case (Real.fromString s) of
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   426
    SOME s => s
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   427
  | NONE => error ("Not a real number: " ^ s)
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   428
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   429
fun read_expectation "no_expectation" = No_Expectation
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   430
  | read_expectation "no_counterexample" = No_Counterexample
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   431
  | read_expectation "counterexample" = Counterexample
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   432
  | read_expectation s = error ("Not an expectation value: " ^ s)
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   433
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   434
fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt)))
40912
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   435
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   436
fun parse_tester name genctxt =
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   437
  if valid_tester_name genctxt name then
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   438
    Config.put_generic tester name genctxt
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   439
  else
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   440
    error ("Unknown tester: " ^ name)
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   441
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   442
fun parse_test_param ("tester", [arg]) = parse_tester arg
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   443
  | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   444
  | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   445
  | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   446
    map_test_params
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   447
      ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   448
  | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   449
  | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   450
  | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   451
  | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   452
  | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
40646
3dfa41e89738 adding option finite_types to quickcheck
bulwahn
parents: 40644
diff changeset
   453
  | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   454
  | parse_test_param ("finite_type_size", [arg]) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   455
    Config.put_generic finite_type_size (read_nat arg)
40912
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   456
  | parse_test_param (name, _) = fn genctxt =>
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   457
    if valid_tester_name genctxt name then
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   458
      Config.put_generic tester name genctxt
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   459
    else error ("Unknown tester or test parameter: " ^ name);
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   460
42025
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   461
fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) =
28336
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   462
      case try (ProofContext.read_typ ctxt) name
42025
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   463
       of SOME (TFree (v, _)) =>
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   464
         ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt)
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   465
        | NONE => (case name of
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   466
            "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt)
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   467
          | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   468
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   469
fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   470
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   471
fun gen_quickcheck args i state =
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   472
  state
42025
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   473
  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   474
  |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state'
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   475
  |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   476
               error ("quickcheck expected to find no counterexample but found one") else ()
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   477
           | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   478
               error ("quickcheck expected to find a counterexample but did not find one") else ()))
32297
3a4081abb3f7 Quickcheck callable from ML
boehmes
parents: 31599
diff changeset
   479
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   480
fun quickcheck args i state = fst (gen_quickcheck args i state);
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   481
32297
3a4081abb3f7 Quickcheck callable from ML
boehmes
parents: 31599
diff changeset
   482
fun quickcheck_cmd args i state =
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   483
  gen_quickcheck args i (Toplevel.proof_of state)
40225
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   484
  |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   485
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   486
val parse_arg =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   487
  Parse.name --
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   488
    (Scan.optional (Parse.$$$ "=" |--
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   489
      (((Parse.name || Parse.float_number) >> single) ||
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   490
        (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   491
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   492
val parse_args =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   493
  Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
28336
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   494
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   495
val _ =
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   496
  Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   497
    (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   498
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   499
val _ =
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   500
  Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   501
    (parse_args -- Scan.optional Parse.nat 1
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   502
      >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   503
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   504
end;
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   505
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   506
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   507
val auto_quickcheck = Quickcheck.auto;