src/Tools/quickcheck.ML
author bulwahn
Wed, 20 Jul 2011 08:16:36 +0200
changeset 43912 13e6a4e70219
parent 43884 59ba3dbd1400
child 43915 ef347714c5c1
permissions -rw-r--r--
exporting function in quickcheck; adapting mutabelle script
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
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
     9
  val quickcheckN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    10
  val genuineN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    11
  val noneN: string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    12
  val unknownN: string
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    13
  val setup: theory -> theory
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    14
  (* configuration *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32297
diff changeset
    15
  val auto: bool Unsynchronized.ref
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 43881
diff changeset
    16
  val batch_tester : string Config.T
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    17
  val size : int Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    18
  val iterations : int Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    19
  val no_assms : bool Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    20
  val report : bool Config.T
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    21
  val timing : bool Config.T
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    22
  val quiet : bool Config.T
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    23
  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
    24
  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
    25
  val finite_type_size : int Config.T
43912
13e6a4e70219 exporting function in quickcheck; adapting mutabelle script
bulwahn
parents: 43884
diff changeset
    26
  val set_active_testers: string list -> Context.generic -> Context.generic
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
    27
  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
    28
  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
    29
  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
    30
  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
    31
    -> Context.generic -> Context.generic
42089
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    32
  datatype report = Report of
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    33
    { iterations : int, raised_match_errors : int,
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    34
      satisfied_assms : int list, positive_concl_tests : int }
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    35
  (* quickcheck's result *)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    36
  datatype result =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    37
    Result of
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    38
     {counterexample : (string * term) list option,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    39
      evaluation_terms : (term * term) list option,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    40
      timings : (string * int) list,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
    41
      reports : (int * report) list}
43314
a9090cabca14 adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents: 43147
diff changeset
    42
  val empty_result : result
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
    43
  val add_timing : (string * int) -> result Unsynchronized.ref -> unit
42089
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    44
  val counterexample_of : result -> (string * term) list option
904897d0c5bd adapting mutabelle; exporting more Quickcheck functions
bulwahn
parents: 42088
diff changeset
    45
  val timings_of : result -> (string * int) list
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    46
  (* registering testers & generators *) 
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    47
  type tester =
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    48
    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    49
  val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    50
  val add_batch_generator :
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
    51
    string * (Proof.context -> term list -> (int -> term list option) list)
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
    52
      -> Context.generic -> Context.generic
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    53
  val add_batch_validator :
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
    54
    string * (Proof.context -> term list -> (int -> bool) list)
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
    55
      -> Context.generic -> Context.generic
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
    56
  (* basic operations *)
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
    57
  type compile_generator =
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
    58
    Proof.context -> (term * term list) list -> int list -> term list option * report option
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
    59
  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
    60
  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
    61
    -> (typ option * (term * term list)) list list
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    62
  val collect_results : ('a -> result) -> 'a list -> result list -> result list
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
    63
  val generator_test_goal_terms : compile_generator ->
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
    64
    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
37910
555287ba8d8d reordering quickcheck signature; exporting test_params and inspection function
bulwahn
parents: 37909
diff changeset
    65
  (* testing terms and proof states *)
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
    66
  val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
43883
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 43882
diff changeset
    67
  val test_goal_terms :
aacbe67793c3 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
bulwahn
parents: 43882
diff changeset
    68
    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
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
    69
  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
    70
  (* testing a batch of terms *)
42188
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
    71
  val test_terms:
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
    72
    Proof.context -> term list -> (string * term) list option list option * (string * int) list
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
    73
  val validate_terms: Proof.context -> term list -> bool list option * (string * int) list
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    74
end;
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    75
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    76
structure Quickcheck : QUICKCHECK =
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    77
struct
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
    78
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    79
val quickcheckN = "quickcheck"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    80
val quickcheck_paramsN = "quickcheck_params"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    81
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    82
val genuineN = "genuine"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    83
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    84
val unknownN = "unknown"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    85
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    86
(* preferences *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    87
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32297
diff changeset
    88
val auto = Unsynchronized.ref false;
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    89
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    90
val _ =
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    91
  ProofGeneralPgip.add_preference Preferences.category_tracing
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39329
diff changeset
    92
  (Unsynchronized.setmp auto true (fn () =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    93
    Preferences.bool_pref auto
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    94
      "auto-quickcheck"
39329
0a85f960ac50 make Auto Solve part of the "Auto Tools"
blanchet
parents: 39324
diff changeset
    95
      "Run Quickcheck automatically.") ());
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
    96
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    97
(* quickcheck report *)
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    98
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
    99
datatype report = Report of
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   100
  { iterations : int, raised_match_errors : int,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   101
    satisfied_assms : int list, positive_concl_tests : int }
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   102
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   103
(* Quickcheck Result *)
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   104
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   105
datatype result = Result of
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   106
  { counterexample : (string * term) list option, evaluation_terms : (term * term) list option,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   107
    timings : (string * int) list, reports : (int * report) list}
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   108
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   109
val empty_result =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   110
  Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   111
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   112
fun counterexample_of (Result r) = #counterexample r
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   113
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   114
fun found_counterexample (Result r) = is_some (#counterexample r)
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   115
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   116
fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   117
    (SOME ts, SOME evals) => SOME (ts, evals)
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   118
  | (NONE, NONE) => NONE
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   119
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   120
fun timings_of (Result r) = #timings r
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   121
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   122
fun set_reponse names eval_terms (SOME ts) (Result r) =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   123
  let
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   124
    val (ts1, ts2) = chop (length names) ts
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   125
  in
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   126
    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms ~~ ts2),
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   127
      timings = #timings r, reports = #reports r}
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   128
  end
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   129
  | set_reponse _ _ NONE result = result
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   130
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   131
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   132
fun set_counterexample counterexample (Result r) =
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   133
  Result {counterexample = counterexample,  evaluation_terms = #evaluation_terms r,
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   134
    timings = #timings r, reports = #reports r}
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   135
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   136
fun set_evaluation_terms evaluation_terms (Result r) =
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   137
  Result {counterexample = #counterexample r,  evaluation_terms = evaluation_terms,
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   138
    timings = #timings r, reports = #reports r}
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   139
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   140
fun cons_timing timing (Result r) =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   141
  Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   142
    timings = cons timing (#timings r), reports = #reports r}
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   143
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   144
fun cons_report size (SOME report) (Result r) =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   145
  Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   146
    timings = #timings r, reports = cons (size, report) (#reports r)}
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   147
  | cons_report _ NONE result = result
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   148
42198
ded5ba6b7bac use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
wenzelm
parents: 42194
diff changeset
   149
fun add_timing timing result_ref =
ded5ba6b7bac use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
wenzelm
parents: 42194
diff changeset
   150
  Unsynchronized.change result_ref (cons_timing timing)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   151
42198
ded5ba6b7bac use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
wenzelm
parents: 42194
diff changeset
   152
fun add_report size report result_ref =
ded5ba6b7bac use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
wenzelm
parents: 42194
diff changeset
   153
  Unsynchronized.change result_ref (cons_report size report)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   154
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   155
fun add_response names eval_terms response result_ref =
42198
ded5ba6b7bac use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
wenzelm
parents: 42194
diff changeset
   156
  Unsynchronized.change result_ref (set_reponse names eval_terms response)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   157
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   158
(* expectation *)
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   159
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   160
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
   161
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   162
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
   163
  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
   164
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   165
(* quickcheck configuration -- default parameters, test generators *)
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 43881
diff changeset
   166
val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   167
val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   168
val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   169
val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   170
val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   171
val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   172
val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   173
val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   174
val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42433
diff changeset
   175
val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
40646
3dfa41e89738 adding option finite_types to quickcheck
bulwahn
parents: 40644
diff changeset
   176
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   177
datatype test_params = Test_Params of
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   178
  {default_type: typ list, expect : expectation};
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   179
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   180
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
   181
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   182
fun make_test_params (default_type, expect) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   183
  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
   184
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   185
fun map_test_params' f (Test_Params {default_type, expect}) =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   186
  make_test_params (f (default_type, expect));
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   187
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   188
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
   189
  (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
   190
    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
   191
  make_test_params
f6ab14e61604 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents: 41086
diff changeset
   192
    (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   193
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   194
type tester =
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   195
  Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   196
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 39138
diff changeset
   197
structure Data = Generic_Data
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33291
diff changeset
   198
(
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   199
  type T =
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   200
    ((string * (bool Config.T * tester)) list
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   201
      * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   202
      * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
38759
37a9092de102 simplification/standardization of some theory data;
wenzelm
parents: 38390
diff changeset
   203
      * test_params;
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   204
  val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   205
  val extend = I;
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   206
  fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   207
    ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   208
    ((AList.merge (op =) (K true) (testers1, testers2),
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
   209
      (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
   210
       AList.merge (op =) (K true) (batch_validators1, batch_validators2))),
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   211
      merge_test_params (params1, params2));
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33291
diff changeset
   212
);
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   213
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 39138
diff changeset
   214
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
   215
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   216
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
   217
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   218
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
   219
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
   220
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
   221
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   222
(*val add_generator = Data.map o apfst o apfst o apfst o AList.update (op =);*)
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
   223
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   224
val add_tester = Data.map o apfst o apfst o AList.update (op =);
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   225
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   226
val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =);
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   227
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   228
val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =);
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   229
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   230
fun active_testers ctxt =
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   231
  let
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   232
    val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   233
  in
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   234
    map snd (filter (fn (active, _) => Config.get ctxt active) testers)
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   235
  end
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   236
  
43884
59ba3dbd1400 quickcheck does not deactivate testers if none are given
bulwahn
parents: 43883
diff changeset
   237
fun set_active_testers [] gen_ctxt = gen_ctxt
59ba3dbd1400 quickcheck does not deactivate testers if none are given
bulwahn
parents: 43883
diff changeset
   238
  | set_active_testers testers gen_ctxt =
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   239
  let
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   240
    val registered_testers = (fst o fst o Data.get) gen_ctxt
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   241
  in
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   242
    fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   243
      registered_testers gen_ctxt
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   244
  end
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   245
    
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   246
(* generating tests *)
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   247
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   248
fun gen_mk_tester lookup ctxt v =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   249
  let
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 43881
diff changeset
   250
    val name = Config.get ctxt batch_tester
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   251
    val tester = case lookup ctxt name
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 43881
diff changeset
   252
      of NONE => error ("No such quickcheck batch-tester: " ^ name)
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   253
      | 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
   254
  in
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   255
    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
   256
      try tester v
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   257
    else
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43585
diff changeset
   258
      let (* FIXME !?!? *)
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   259
        val tester = Exn.interruptible_capture tester v
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 43585
diff changeset
   260
      in case Exn.get_res tester of
40909
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   261
          NONE => SOME (Exn.release tester)
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   262
        | SOME tester => SOME tester
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   263
      end
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   264
  end
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 43881
diff changeset
   265
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   266
val mk_batch_tester =
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   267
  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   268
val mk_batch_validator =
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   269
  gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt))
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
   270
  
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   271
fun lookup_tester ctxt = AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)
43112
3117573292b8 adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
bulwahn
parents: 43029
diff changeset
   272
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   273
(* testing propositions *)
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   274
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   275
type compile_generator =
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   276
  Proof.context -> (term * term list) list -> int list -> term list option * report option
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   277
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   278
fun check_test_term t =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   279
  let
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28952
diff changeset
   280
    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
   281
      error "Term to be tested contains type variables";
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28952
diff changeset
   282
    val _ = null (Term.add_vars t []) orelse
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   283
      error "Term to be tested contains schematic variables";
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   284
  in () end
28256
4e7f7d52f855 added quickcheck.ML
haftmann
parents:
diff changeset
   285
42014
75417ef605ba simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents: 42012
diff changeset
   286
fun cpu_time description e =
75417ef605ba simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents: 42012
diff changeset
   287
  let val ({cpu, ...}, result) = Timing.timing e ()
75417ef605ba simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents: 42012
diff changeset
   288
  in (result, (description, Time.toMilliseconds cpu)) end
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   289
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   290
fun limit timeout (limit_time, is_interactive) f exc () =
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   291
  if limit_time then
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   292
      TimeLimit.timeLimit timeout f ()
41754
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   293
    handle TimeLimit.TimeOut =>
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   294
      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
   295
  else
aa94a003dcdf quickcheck can be invoked with its internal timelimit or without
bulwahn
parents: 41753
diff changeset
   296
    f ()
41753
dbd00d8a4784 quickcheck invokes TimeLimit.timeLimit only in one separate function
bulwahn
parents: 41735
diff changeset
   297
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   298
fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   299
  let
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   300
    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   301
    val _ = check_test_term t
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   302
    val names = Term.add_free_names t []
40366
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   303
    val current_size = Unsynchronized.ref 0
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   304
    val current_result = Unsynchronized.ref empty_result 
42087
5e236f6ef04f changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
bulwahn
parents: 42032
diff changeset
   305
    fun excipit () =
5e236f6ef04f changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
bulwahn
parents: 42032
diff changeset
   306
      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   307
    fun with_size test_fun k =
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   308
      if k > Config.get ctxt size then
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   309
        NONE
40911
7febf76e0a69 moving iteration of tests to the testers in quickcheck
bulwahn
parents: 40910
diff changeset
   310
      else
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   311
        let
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   312
          val _ = message ("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
   313
          val _ = current_size := k
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   314
          val ((result, report), timing) =
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42089
diff changeset
   315
            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   316
          val _ = add_timing timing current_result
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   317
          val _ = add_report k report current_result
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   318
        in
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   319
          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   320
        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
   321
  in
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   322
    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   323
      let
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   324
        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   325
          (fn () => compile ctxt [(t, eval_terms)]);
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   326
        val _ = add_timing comp_time current_result
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   327
        val (response, exec_time) =
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   328
          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   329
        val _ = add_response names eval_terms response current_result
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   330
        val _ = add_timing exec_time current_result
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   331
      in !current_result end)
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   332
    (fn () => (message (excipit ()); !current_result)) ()
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   333
  end;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   334
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   335
fun validate_terms ctxt ts =
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   336
  let
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   337
    val _ = map check_test_term ts
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   338
    val size = Config.get ctxt size
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   339
    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   340
      (fn () => mk_batch_validator ctxt ts) 
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   341
    fun with_size tester k =
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   342
      if k > size then true
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   343
      else if tester k then with_size tester (k + 1) else false
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   344
    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   345
        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   346
              (fn () => with_size test_fun 1) ()
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   347
             handle TimeLimit.TimeOut => true)) test_funs)
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   348
  in
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   349
    (results, [comp_time, exec_time])
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   350
  end
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   351
  
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   352
fun test_terms ctxt ts =
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   353
  let
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   354
    val _ = map check_test_term ts
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   355
    val size = Config.get ctxt size
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   356
    val namess = map (fn t => Term.add_free_names t []) ts
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   357
    val (test_funs, comp_time) =
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   358
      cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) 
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   359
    fun with_size tester k =
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   360
      if k > size then NONE
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   361
      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
42188
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
   362
    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
   363
        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
42194
bd416284a432 adding general interface for batch validators in quickcheck
bulwahn
parents: 42188
diff changeset
   364
              (fn () => with_size test_fun 1) ()
42188
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
   365
             handle TimeLimit.TimeOut => NONE)) test_funs)
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   366
  in
42188
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
   367
    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
f6bc441fbf19 adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
bulwahn
parents: 42162
diff changeset
   368
      [comp_time, exec_time])
41862
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   369
  end
a38536bf2736 adding function Quickcheck.test_terms to provide checking a batch of terms
bulwahn
parents: 41754
diff changeset
   370
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
   371
(* 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
   372
(* 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
   373
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   374
fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   375
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42275
diff changeset
   376
    val thy = Proof_Context.theory_of ctxt
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   377
    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42089
diff changeset
   378
    val (ts', eval_terms) = split_list ts
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42089
diff changeset
   379
    val _ = map check_test_term ts'
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42089
diff changeset
   380
    val names = Term.add_free_names (hd ts') []
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42089
diff changeset
   381
    val Ts = map snd (Term.add_frees (hd ts') [])
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   382
    val current_result = Unsynchronized.ref empty_result
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   383
    fun test_card_size test_fun (card, size) =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   384
      (* FIXME: why decrement size by one? *)
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   385
      let
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   386
        val (ts, timing) =
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   387
          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   388
            (fn () => fst (test_fun [card, size - 1]))
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   389
        val _ = add_timing timing current_result
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   390
      in
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   391
        Option.map (pair card) ts
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   392
      end
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   393
    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
   394
      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
   395
        (* 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
   396
        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
   397
      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
   398
        (* 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
   399
        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
   400
        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   401
  in
43585
ea959ab7bbe3 adding timeout to quickcheck narrowing
bulwahn
parents: 43314
diff changeset
   402
    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   403
      let
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   404
        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   405
        val _ = add_timing comp_time current_result     
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   406
        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   407
          SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   408
        | NONE => ()
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   409
      in !current_result end)
42162
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   410
      (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
00899500c6ca moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
bulwahn
parents: 42159
diff changeset
   411
  end
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   412
40647
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   413
fun get_finite_types ctxt =
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   414
  fst (chop (Config.get ctxt finite_type_size)
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   415
    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   416
     "Enum.finite_4", "Enum.finite_5"]))
40647
6e92ca8e981b adding prototype for finite_type instantiations
bulwahn
parents: 40646
diff changeset
   417
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   418
exception WELLSORTED of string
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   419
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   420
fun monomorphic_term thy insts default_T =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   421
  let
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   422
    fun subst (T as TFree (v, S)) =
40903
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   423
      let
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   424
        val T' = AList.lookup (op =) insts v
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   425
          |> the_default default_T
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   426
      in if Sign.of_sort thy (T', S) then T'
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   427
        else raise (WELLSORTED ("For instantiation with default_type " ^
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   428
          Syntax.string_of_typ_global thy default_T ^
40903
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   429
          ":\n" ^ Syntax.string_of_typ_global thy T' ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   430
          " to be substituted for variable " ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   431
          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   432
          Syntax.string_of_sort_global thy S))
1332f6e856b9 corrected indentation
bulwahn
parents: 40656
diff changeset
   433
      end
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   434
      | subst T = T;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   435
  in (map_types o map_atyps) subst end;
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   436
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   437
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   438
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   439
fun instantiate_goals lthy insts goals =
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   440
  let
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   441
    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42275
diff changeset
   442
    val thy = Proof_Context.theory_of lthy
40926
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   443
    val default_insts =
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   444
      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
   445
    val inst_goals =
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   446
      map (fn (check_goal, eval_terms) =>
40926
c600f6ae4b09 only instantiate type variable if there exists some in quickcheck
bulwahn
parents: 40916
diff changeset
   447
        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
   448
          map (fn T =>
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   449
            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   450
              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   451
              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
   452
        else
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   453
          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   454
    val error_msg =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   455
      cat_lines
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   456
        (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
   457
    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
   458
      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   459
    val correct_inst_goals =
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   460
      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
   461
        [[]] => error error_msg
37913
e85f5ad02a8f correcting wellsortedness check and improving error message
bulwahn
parents: 37912
diff changeset
   462
      | xs => xs
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   463
    val _ = if Config.get lthy quiet then () else warning error_msg
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   464
  in
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   465
    correct_inst_goals
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   466
  end
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   467
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   468
fun collect_results f [] results = results
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   469
  | collect_results f (t :: ts) results =
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   470
    let
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   471
      val result = f t
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   472
    in
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   473
      if found_counterexample result then
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   474
        (result :: results)
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   475
      else
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   476
        collect_results f ts (result :: results)
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   477
    end  
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   478
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   479
fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   480
  let
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   481
    fun test_term' goal =
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   482
      case goal of
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   483
        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   484
      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
43147
70337ff0352d moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
bulwahn
parents: 43114
diff changeset
   485
    val correct_inst_goals = instantiate_goals ctxt insts goals
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   486
  in
43875
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   487
    if Config.get ctxt finite_types then
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   488
      collect_results test_term' correct_inst_goals []
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   489
    else
43876
b8fa7287ee4c parametrized test_term functions in quickcheck
bulwahn
parents: 43875
diff changeset
   490
      collect_results (test_term compile ctxt (limit_time, is_interactive))
43875
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   491
        (maps (map snd) correct_inst_goals) []
41043
3750bdac1327 testing smartly in two dimensions (cardinality and size) in quickcheck
bulwahn
parents: 40931
diff changeset
   492
  end;
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   493
  
43875
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   494
fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   495
  case active_testers ctxt of
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   496
    [] => error "No active testers for quickcheck"
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   497
  | testers => testers |> Par_List.get_some (fn tester =>
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   498
      tester ctxt (limit_time, is_interactive) insts goals |>
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   499
      (fn result => if exists found_counterexample result then SOME result else NONE))
43875
485d2ad43528 adding random, exhaustive and SML quickcheck as testers
bulwahn
parents: 43761
diff changeset
   500
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   501
fun test_goal (time_limit, is_interactive) (insts, eval_terms) 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
   502
  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
   503
    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
   504
    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
   505
    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
   506
      | 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
   507
    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
   508
    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
   509
    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
   510
     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
   511
      | 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
   512
      | 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
   513
    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
   514
     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
   515
      | 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
   516
    val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
43113
7226051e8b89 splitting test_goal_terms in Quickcheck into smaller basic functions
bulwahn
parents: 43112
diff changeset
   517
    val goals = case some_locale
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   518
     of NONE => [(proto_goal, eval_terms)]
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   519
      | SOME locale =>
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   520
        map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   521
          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
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
   522
  in
43147
70337ff0352d moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
bulwahn
parents: 43114
diff changeset
   523
    test_goal_terms lthy (time_limit, is_interactive) insts 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
   524
  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
   525
37912
247042107f93 using multiple default types in quickcheck
bulwahn
parents: 37911
diff changeset
   526
(* pretty printing *)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   527
40225
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   528
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   529
2de5dd0cd3a2 clear identification
blanchet
parents: 40148
diff changeset
   530
fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   531
  | pretty_counterex ctxt auto (SOME (cex, eval_terms)) =
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   532
      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   533
        map (fn (s, t) =>
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42026
diff changeset
   534
          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   535
        @ (if null eval_terms then []
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   536
           else (Pretty.str ("Evaluated terms:\n") ::
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   537
             map (fn (t, u) =>
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   538
               Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   539
                 Syntax.pretty_term ctxt u]) (rev eval_terms))));
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   540
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   541
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
   542
    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   543
  let
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   544
    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
   545
  in
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   546
     ([pretty_stat "iterations" iterations,
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   547
     pretty_stat "match exceptions" raised_match_errors]
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   548
     @ map_index
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   549
       (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
   550
       satisfied_assms
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   551
     @ [pretty_stat "positive conclusion tests" positive_concl_tests])
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   552
  end
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   553
35380
6ac5b81a763d adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents: 35379
diff changeset
   554
fun pretty_reports ctxt (SOME reports) =
40916
9928083506b6 improving presentation of quickcheck reports
bulwahn
parents: 40912
diff changeset
   555
  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
   556
    maps (fn (size, report) =>
e006d1e06920 renamed parameter from generator to tester; quickcheck only applies one tester on invocation
bulwahn
parents: 40908
diff changeset
   557
      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
   558
      (rev reports))
35380
6ac5b81a763d adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
bulwahn
parents: 35379
diff changeset
   559
  | pretty_reports ctxt NONE = Pretty.str ""
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   560
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   561
fun pretty_timings timings =
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   562
  Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   563
    maps (fn (label, time) =>
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   564
      Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   565
42433
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   566
fun pretty_counterex_and_reports ctxt auto [] =
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   567
    Pretty.chunks [Pretty.strs (tool_name auto ::
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   568
        space_explode " " "is used in a locale where no interpretation is provided."),
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   569
      Pretty.strs (space_explode " " "Please provide an executable interpretation for the locale.")]
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   570
  | pretty_counterex_and_reports ctxt auto (result :: _) =
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   571
    Pretty.chunks (pretty_counterex ctxt auto (response_of result) ::
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   572
      (* map (pretty_reports ctxt) (reports_of result) :: *)
b48d9186e883 handling the case where quickcheck is used in a locale with no known interpretation user-friendly
bulwahn
parents: 42361
diff changeset
   573
      (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   574
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 30973
diff changeset
   575
(* Isar commands *)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   576
28336
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   577
fun read_nat s = case (Library.read_int o Symbol.explode) s
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   578
 of (k, []) => if k >= 0 then k
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   579
      else error ("Not a natural number: " ^ s)
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   580
  | (_, _ :: _) => 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
   581
34128
8650a073dd9b made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents: 33583
diff changeset
   582
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
   583
  | read_bool "true" = true
8650a073dd9b made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
blanchet
parents: 33583
diff changeset
   584
  | read_bool s = error ("Not a Boolean value: " ^ s)
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   585
40366
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   586
fun read_real s =
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   587
  case (Real.fromString s) of
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   588
    SOME s => s
a2866dbfbe6b changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn
parents: 40253
diff changeset
   589
  | 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
   590
37929
22e0797857e6 adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
bulwahn
parents: 37913
diff changeset
   591
fun read_expectation "no_expectation" = No_Expectation
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   592
  | 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
   593
  | read_expectation "counterexample" = Counterexample
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   594
  | 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
   595
43877
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   596
fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name
abd1f074cb98 removing generator registration
bulwahn
parents: 43876
diff changeset
   597
  
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   598
fun parse_tester name (testers, genctxt) =
40912
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   599
  if valid_tester_name genctxt name then
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   600
    (insert (op =) name testers, genctxt)  
40912
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   601
  else
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   602
    error ("Unknown tester: " ^ name)
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   603
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   604
fun parse_test_param ("tester", args) = fold parse_tester args
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   605
  | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   606
  | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   607
  | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   608
    (testers, map_test_params
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   609
      ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   610
  | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   611
  | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   612
  | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   613
  | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   614
  | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   615
  | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   616
  | parse_test_param ("finite_type_size", [arg]) =
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   617
    apsnd (Config.put_generic finite_type_size (read_nat arg))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   618
  | parse_test_param (name, _) = (fn (testers, genctxt) =>
40912
1108529100ce checking if parameter is name of a tester which allows e.g. quickcheck[random]
bulwahn
parents: 40911
diff changeset
   619
    if valid_tester_name genctxt name then
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   620
      (insert (op =) name testers, genctxt)  
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   621
    else error ("Unknown tester or test parameter: " ^ name));
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   622
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   623
fun proof_map_result f = apsnd Context.the_proof o f o Context.Proof;
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   624
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   625
fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42275
diff changeset
   626
      case try (Proof_Context.read_typ ctxt) name
42025
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   627
       of SOME (TFree (v, _)) =>
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   628
         ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms),
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   629
           (testers, ctxt))
42025
cb5b1e85b32e adding eval option to quickcheck
bulwahn
parents: 41862
diff changeset
   630
        | NONE => (case name of
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   631
            "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   632
          | _ => ((insts, eval_terms),
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   633
            proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   634
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   635
fun quickcheck_params_cmd args = Context.theory_map
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   636
  (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   637
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   638
fun check_expectation state results =
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   639
  (if is_some results andalso expect (Proof.context_of state) = No_Counterexample
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   640
  then
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   641
    error ("quickcheck expected to find no counterexample but found one")
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   642
  else
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   643
    (if is_none results andalso expect (Proof.context_of state) = Counterexample
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   644
    then
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   645
      error ("quickcheck expected to find a counterexample but did not find one")
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   646
    else ()))
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   647
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   648
fun gen_quickcheck args i state =
40644
0850a2a16dce changed old-style quickcheck configurations to new Config.T configurations
bulwahn
parents: 40643
diff changeset
   649
  state
43881
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   650
  |> Proof.map_context_result (fn ctxt =>
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   651
    apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
cabe74eab19a changing parser in quickcheck to activate and deactivate the testers
bulwahn
parents: 43879
diff changeset
   652
      (fold parse_test_param_inst args (([], []), ([], ctxt))))
42026
da9b58f1db42 adding option of evaluating terms after invocation in quickcheck
bulwahn
parents: 42025
diff changeset
   653
  |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
42088
8d00484551fe making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn
parents: 42087
diff changeset
   654
  |> tap (check_expectation state'))
32297
3a4081abb3f7 Quickcheck callable from ML
boehmes
parents: 31599
diff changeset
   655
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   656
fun quickcheck args i state =
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   657
  Option.map (the o get_first counterexample_of) (gen_quickcheck args i state)
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   658
32297
3a4081abb3f7 Quickcheck callable from ML
boehmes
parents: 31599
diff changeset
   659
fun quickcheck_cmd args i state =
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35324
diff changeset
   660
  gen_quickcheck args i (Toplevel.proof_of state)
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   661
  |> Option.map (the o get_first response_of)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   662
  |> Output.urgent_message o Pretty.string_of
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   663
     o pretty_counterex (Toplevel.context_of state) false;
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   664
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   665
val parse_arg =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   666
  Parse.name --
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   667
    (Scan.optional (Parse.$$$ "=" |--
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   668
      (((Parse.name || Parse.float_number) >> single) ||
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   669
        (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   670
41517
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   671
val parse_args =
7267fb5b724b observe line length limit;
wenzelm
parents: 41472
diff changeset
   672
  Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
28336
a8edf4c69a79 fixed quickcheck parameter syntax
haftmann
parents: 28315
diff changeset
   673
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   674
val _ =
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   675
  Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   676
    (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   677
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   678
val _ =
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   679
  Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   680
    (parse_args -- Scan.optional Parse.nat 1
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   681
      >> (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
   682
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   683
(* automatic testing *)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   684
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   685
fun try_quickcheck auto state =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   686
  let
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   687
    val ctxt = Proof.context_of state;
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   688
    val i = 1;
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   689
    val res =
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   690
      state
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   691
      |> Proof.map_context (Config.put report false #> Config.put quiet true)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   692
      |> try (test_goal (false, false) ([], []) i);
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   693
  in
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   694
    case res of
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   695
      NONE => (unknownN, state)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   696
    | SOME results =>
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   697
        let
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   698
          val msg = pretty_counterex ctxt auto (Option.map (the o get_first response_of) results)
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   699
        in
43879
c8308a8faf9f enabling parallel execution of testers but removing more informative quickcheck output
bulwahn
parents: 43878
diff changeset
   700
          if is_some results then
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   701
            (genuineN,
43029
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   702
             state
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   703
             |> (if auto then
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   704
                   Proof.goal_message (K (Pretty.chunks [Pretty.str "",
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   705
                       Pretty.mark Markup.hilite msg]))
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   706
                 else
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   707
                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   708
          else
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   709
            (noneN, state)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   710
        end
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   711
  end
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   712
  |> `(fn (outcome_code, _) => outcome_code = genuineN)
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   713
43029
3e060b1c844b use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
blanchet
parents: 43024
diff changeset
   714
val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck))
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   715
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   716
end;
28309
c24bc53c815c some steps towards generic quickcheck framework
haftmann
parents: 28256
diff changeset
   717
28315
d3cf88fe77bc generic quickcheck framework
haftmann
parents: 28309
diff changeset
   718
val auto_quickcheck = Quickcheck.auto;