author  bulwahn 
Mon, 23 Jan 2012 14:06:19 +0100  
changeset 46312  518cc38a1a8c 
parent 45923  473b744c23f2 
child 46327  ecda23528833 
permissions  rwrr 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

1 
(* Title: HOL/Tools/Quickcheck/quickcheck_common.ML 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

2 
Author: Florian Haftmann, Lukas Bulwahn, TU Muenchen 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

3 

41938  4 
Common functions for quickcheck's generators. 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

5 
*) 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

6 

8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

7 
signature QUICKCHECK_COMMON = 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

8 
sig 
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

9 
val strip_imp : term > (term list * term) 
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset

10 
val reflect_bool : bool > term 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

11 
val define_functions : ((term list > term list) * (Proof.context > tactic) option) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

12 
> string > string list > string list > typ list > Proof.context > Proof.context 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

13 
val perhaps_constrain: theory > (typ * sort) list > (string * sort) list 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

14 
> (string * sort > string * sort) option 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

15 
val instantiate_goals: Proof.context > (string * typ) list > (term * term list) list 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

16 
> (typ option * (term * term list)) list list 
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

17 
val mk_safe_if : term > term > term * term * (bool > term) > bool > term 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

18 
val collect_results : ('a > Quickcheck.result) > 'a list > Quickcheck.result list > Quickcheck.result list 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

19 
type compile_generator = 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

20 
Proof.context > (term * term list) list > bool > int list > (bool * term list) option * Quickcheck.report option 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

21 
val generator_test_goal_terms : 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

22 
string * compile_generator > Proof.context > bool > (string * typ) list 
45418  23 
> (term * term list) list > Quickcheck.result list 
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

24 
type instantiation = Datatype.config > Datatype.descr > (string * sort) list 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

25 
> string list > string > string list * string list > typ list * typ list > theory > theory 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

26 
val ensure_sort : 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

27 
(((sort * sort) * sort) * 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

28 
((theory > string list > Datatype_Aux.descr * (string * sort) list * string list 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

29 
* string * (string list * string list) * (typ list * typ list)) * instantiation)) 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

30 
> Datatype.config > string list > theory > theory 
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

31 
val ensure_common_sort_datatype : 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

32 
(sort * instantiation) > Datatype.config > string list > theory > theory 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

33 
val datatype_interpretation : (sort * instantiation) > theory > theory 
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:
42110
diff
changeset

34 
val gen_mk_parametric_generator_expr : 
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

35 
(((Proof.context > term * term list > term) * term) * typ) 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

36 
> Proof.context > (term * term list) list > term 
45039
632a033616e9
adding postprocessing of terms to narrowingbased Quickcheck
bulwahn
parents:
44241
diff
changeset

37 
val mk_fun_upd : typ > typ > term * term > term > term 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

38 
val post_process_term : term > term 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

39 
val test_term : string * compile_generator 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

40 
> Proof.context > bool > term * term list > Quickcheck.result 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

41 
end; 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

42 

8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

43 
structure Quickcheck_Common : QUICKCHECK_COMMON = 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

44 
struct 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

45 

42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

46 
(* static options *) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

47 

9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

48 
val define_foundationally = false 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

49 

42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

50 
(* HOLogic's term functions *) 
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

51 

1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

52 
fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) 
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

53 
 strip_imp A = ([], A) 
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset

54 

45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset

55 
fun reflect_bool b = if b then @{term "True"} else @{term "False"} 
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset

56 

42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

57 
fun mk_undefined T = Const(@{const_name undefined}, T) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

58 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

59 
(* testing functions: testing with increasing sizes (and cardinalities) *) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

60 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

61 
type compile_generator = 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

62 
Proof.context > (term * term list) list > bool > int list > (bool * term list) option * Quickcheck.report option 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

63 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

64 
fun check_test_term t = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

65 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

66 
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

67 
error "Term to be tested contains type variables"; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

68 
val _ = null (Term.add_vars t []) orelse 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

69 
error "Term to be tested contains schematic variables"; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

70 
in () end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

71 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

72 
fun cpu_time description e = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

73 
let val ({cpu, ...}, result) = Timing.timing e () 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

74 
in (result, (description, Time.toMilliseconds cpu)) end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

75 

45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

76 
fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) = 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

77 
let 
45757
e32dd098f57a
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents:
45755
diff
changeset

78 
val genuine_only = Config.get ctxt Quickcheck.genuine_only 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

79 
val _ = check_test_term t 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

80 
val names = Term.add_free_names t [] 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

81 
val current_size = Unsynchronized.ref 0 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

82 
val current_result = Unsynchronized.ref Quickcheck.empty_result 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

83 
fun excipit () = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

84 
"Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

85 
val act = if catch_code_errors then try else (fn f => SOME o f) 
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

86 
val (test_fun, comp_time) = cpu_time "quickcheck compilation" 
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

87 
(fn () => act (compile ctxt) [(t, eval_terms)]); 
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

88 
val _ = Quickcheck.add_timing comp_time current_result 
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

89 
fun with_size test_fun genuine_only k = 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

90 
if k > Config.get ctxt Quickcheck.size then 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

91 
NONE 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

92 
else 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

93 
let 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

94 
val _ = Quickcheck.verbose_message ctxt 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

95 
("[Quickcheck" ^ name ^ "] Test data size: " ^ string_of_int k) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

96 
val _ = current_size := k 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

97 
val ((result, report), timing) = 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

98 
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k  1]) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

99 
val _ = Quickcheck.add_timing timing current_result 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

100 
val _ = Quickcheck.add_report k report current_result 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

101 
in 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

102 
case result of 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

103 
NONE => with_size test_fun genuine_only (k + 1) 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

104 
 SOME (true, ts) => SOME (true, ts) 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

105 
 SOME (false, ts) => 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

106 
let 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

107 
val (ts1, ts2) = chop (length names) ts 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

108 
val (eval_terms', _) = chop (length ts2) eval_terms 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

109 
val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

110 
in 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

111 
(Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

112 
Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

113 
with_size test_fun true k) 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

114 
end 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

115 
end; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

116 
in 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

117 
case test_fun of 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

118 
NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck" ^ name); 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

119 
!current_result) 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

120 
 SOME test_fun => 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

121 
let 
45819  122 
val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck" ^ name ^ "..."); 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

123 
val (response, exec_time) = 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

124 
cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

125 
val _ = Quickcheck.add_response names eval_terms response current_result 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

126 
val _ = Quickcheck.add_timing exec_time current_result 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

127 
in !current_result end 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

128 
end; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

129 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

130 
fun validate_terms ctxt ts = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

131 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

132 
val _ = map check_test_term ts 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

133 
val size = Config.get ctxt Quickcheck.size 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

134 
val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

135 
(fn () => Quickcheck.mk_batch_validator ctxt ts) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

136 
fun with_size tester k = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

137 
if k > size then true 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

138 
else if tester k then with_size tester (k + 1) else false 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

139 
val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

140 
Option.map (map (fn test_fun => 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

141 
TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

142 
(fn () => with_size test_fun 1) () 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

143 
handle TimeLimit.TimeOut => true)) test_funs) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

144 
in 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

145 
(results, [comp_time, exec_time]) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

146 
end 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

147 

45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

148 
fun test_terms ctxt ts = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

149 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

150 
val _ = map check_test_term ts 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

151 
val size = Config.get ctxt Quickcheck.size 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

152 
val namess = map (fn t => Term.add_free_names t []) ts 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

153 
val (test_funs, comp_time) = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

154 
cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

155 
fun with_size tester k = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

156 
if k > size then NONE 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

157 
else case tester k of SOME ts => SOME ts  NONE => with_size tester (k + 1) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

158 
val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

159 
Option.map (map (fn test_fun => 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

160 
TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

161 
(fn () => with_size test_fun 1) () 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

162 
handle TimeLimit.TimeOut => NONE)) test_funs) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

163 
in 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

164 
(Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results, 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

165 
[comp_time, exec_time]) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

166 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

167 

45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

168 
fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts = 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

169 
let 
45757
e32dd098f57a
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents:
45755
diff
changeset

170 
val genuine_only = Config.get ctxt Quickcheck.genuine_only 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

171 
val thy = Proof_Context.theory_of ctxt 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

172 
val (ts', eval_terms) = split_list ts 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

173 
val _ = map check_test_term ts' 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

174 
val names = Term.add_free_names (hd ts') [] 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

175 
val Ts = map snd (Term.add_frees (hd ts') []) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

176 
val current_result = Unsynchronized.ref Quickcheck.empty_result 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

177 
fun test_card_size test_fun genuine_only (card, size) = 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

178 
(* FIXME: why decrement size by one? *) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

179 
let 
45686
cf22004ad55d
adding more verbose messages to exhaustive quickcheck
bulwahn
parents:
45639
diff
changeset

180 
val _ = 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

181 
Quickcheck.verbose_message ctxt ("[Quickcheck" ^ name ^ "] Test " ^ 
45686
cf22004ad55d
adding more verbose messages to exhaustive quickcheck
bulwahn
parents:
45639
diff
changeset

182 
(if size = 0 then "" else "data size: " ^ string_of_int (size  1) ^ " and ") ^ 
cf22004ad55d
adding more verbose messages to exhaustive quickcheck
bulwahn
parents:
45639
diff
changeset

183 
"cardinality: " ^ string_of_int card) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

184 
val (ts, timing) = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

185 
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

186 
(fn () => fst (test_fun genuine_only [card, size  1])) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

187 
val _ = Quickcheck.add_timing timing current_result 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

188 
in 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

189 
Option.map (pair (card, size)) ts 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

190 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

191 
val enumeration_card_size = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

192 
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

193 
(* size does not matter *) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

194 
map (rpair 0) (1 upto (length ts)) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

195 
else 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

196 
(* size does matter *) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

197 
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

198 
> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) 
45419
10ba32c347b0
quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents:
45418
diff
changeset

199 
val act = if catch_code_errors then try else (fn f => SOME o f) 
10ba32c347b0
quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents:
45418
diff
changeset

200 
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts) 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

201 
val _ = Quickcheck.add_timing comp_time current_result 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

202 
in 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

203 
case test_fun of 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

204 
NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck" ^ name); 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

205 
!current_result) 
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset

206 
 SOME test_fun => 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

207 
let 
45921  208 
val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck" ^ name ^ "..."); 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

209 
fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

210 
SOME ((card, _), (true, ts)) => 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

211 
Quickcheck.add_response names (nth eval_terms (card  1)) (SOME (true, ts)) current_result 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

212 
 SOME ((card, size), (false, ts)) => 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

213 
let 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

214 
val (ts1, ts2) = chop (length names) ts 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

215 
val (eval_terms', _) = chop (length ts2) (nth eval_terms (card  1)) 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

216 
val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

217 
in 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

218 
(Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset

219 
Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

220 
test true (snd (take_prefix (fn x => not (x = (card, size))) enum))) 
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

221 
end 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

222 
 NONE => () 
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset

223 
in (test genuine_only enumeration_card_size; !current_result) end 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

224 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

225 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

226 
fun get_finite_types ctxt = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

227 
fst (chop (Config.get ctxt Quickcheck.finite_type_size) 
45416  228 
[@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"}, 
229 
@{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}]) 

45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

230 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

231 
exception WELLSORTED of string 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

232 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

233 
fun monomorphic_term thy insts default_T = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

234 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

235 
fun subst (T as TFree (v, S)) = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

236 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

237 
val T' = AList.lookup (op =) insts v 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

238 
> the_default default_T 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

239 
in if Sign.of_sort thy (T', S) then T' 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

240 
else raise (WELLSORTED ("For instantiation with default_type " ^ 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

241 
Syntax.string_of_typ_global thy default_T ^ 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

242 
":\n" ^ Syntax.string_of_typ_global thy T' ^ 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

243 
" to be substituted for variable " ^ 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

244 
Syntax.string_of_typ_global thy T ^ " does not have sort " ^ 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

245 
Syntax.string_of_sort_global thy S)) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

246 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

247 
 subst T = T; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

248 
in (map_types o map_atyps) subst end; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

249 

3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

250 
datatype wellsorted_error = Wellsorted_Error of string  Term of term * term list 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

251 

45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

252 
(* minimalistic preprocessing *) 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

253 

9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

254 
fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

255 
let 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

256 
val (a', t') = strip_all t 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

257 
in ((a, T) :: a', t') end 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

258 
 strip_all t = ([], t); 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

259 

9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

260 
fun preprocess ctxt t = 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

261 
let 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

262 
val thy = Proof_Context.theory_of ctxt 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

263 
val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

264 
val rewrs = map (swap o dest) @{thms all_simps} @ 
46312  265 
(map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}]) 
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

266 
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t) 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

267 
val (vs, body) = strip_all t' 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

268 
val vs' = Variable.variant_frees ctxt [t'] vs 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

269 
in 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

270 
subst_bounds (map Free (rev vs'), body) 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

271 
end 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

272 

9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

273 
(* instantiation of type variables with concrete types *) 
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

274 

45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

275 
fun instantiate_goals lthy insts goals = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

276 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

277 
fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

278 
val thy = Proof_Context.theory_of lthy 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

279 
val default_insts = 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

280 
if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

281 
val inst_goals = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

282 
map (fn (check_goal, eval_terms) => 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

283 
if not (null (Term.add_tfree_names check_goal [])) then 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

284 
map (fn T => 
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

285 
(pair (SOME T) o Term o apfst (preprocess lthy)) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

286 
(map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

287 
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

288 
else 
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset

289 
[(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

290 
val error_msg = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

291 
cat_lines 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

292 
(maps (map_filter (fn (_, Term t) => NONE  (_, Wellsorted_Error s) => SOME s)) inst_goals) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

293 
fun is_wellsorted_term (T, Term t) = SOME (T, t) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

294 
 is_wellsorted_term (_, Wellsorted_Error s) = NONE 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

295 
val correct_inst_goals = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

296 
case map (map_filter is_wellsorted_term) inst_goals of 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

297 
[[]] => error error_msg 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

298 
 xs => xs 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

299 
val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

300 
in 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

301 
correct_inst_goals 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

302 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

303 

45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset

304 
(* compilation of testing functions *) 
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset

305 

45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

306 
fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine = 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

307 
let 
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

308 
val T = fastype_of then_t 
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset

309 
val if_t = Const (@{const_name "If"}, @{typ bool} > T > T > T) 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

310 
in 
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

311 
Const (@{const_name "Quickcheck.catch_match"}, T > T > T) $ 
45761
90028fd2f1fa
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents:
45757
diff
changeset

312 
(if_t $ cond $ then_t $ else_t genuine) $ 
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset

313 
(if_t $ genuine_only $ none $ else_t false) 
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset

314 
end 
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset

315 

45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

316 
fun collect_results f [] results = results 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

317 
 collect_results f (t :: ts) results = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

318 
let 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

319 
val result = f t 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

320 
in 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

321 
if Quickcheck.found_counterexample result then 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

322 
(result :: results) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

323 
else 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

324 
collect_results f ts (result :: results) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

325 
end 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

326 

45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

327 
fun generator_test_goal_terms (name, compile) ctxt catch_code_errors insts goals = 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

328 
let 
45687
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset

329 
fun add_eval_term t ts = if is_Free t then ts else ts @ [t] 
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset

330 
fun add_equation_eval_terms (t, eval_terms) = 
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset

331 
case try HOLogic.dest_eq (snd (strip_imp t)) of 
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset

332 
SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms)) 
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset

333 
 NONE => (t, eval_terms) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

334 
fun test_term' goal = 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

335 
case goal of 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

336 
[(NONE, t)] => test_term (name, compile) ctxt catch_code_errors t 
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

337 
 ts => test_term_with_cardinality (name, compile) ctxt catch_code_errors (map snd ts) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

338 
val goals' = instantiate_goals ctxt insts goals 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

339 
> map (map (apsnd add_equation_eval_terms)) 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

340 
in 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

341 
if Config.get ctxt Quickcheck.finite_types then 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

342 
collect_results test_term' goals' [] 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

343 
else 
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset

344 
collect_results (test_term (name, compile) ctxt catch_code_errors) 
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

345 
(maps (map snd) goals') [] 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

346 
end; 
3f1d1ce024cb
moving some common functions from quickcheck to the more HOLspecific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset

347 

42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

348 
(* defining functions *) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

349 

9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

350 
fun pat_completeness_auto ctxt = 
42793  351 
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

352 

9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

353 
fun define_functions (mk_equations, termination_tac) prfx argnames names Ts = 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

354 
if define_foundationally andalso is_some termination_tac then 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

355 
let 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

356 
val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

357 
in 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

358 
Function.add_function 
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset

359 
(map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn)) 
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset

360 
(names ~~ Ts)) 
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset

361 
(map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t) 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

362 
Function_Common.default_config pat_completeness_auto 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

363 
#> snd 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

364 
#> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

365 
#> snd 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

366 
end 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

367 
else 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

368 
fold_map (fn (name, T) => Local_Theory.define 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

369 
((Binding.conceal (Binding.name name), NoSyn), 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

370 
(apfst Binding.conceal Attrib.empty_binding, mk_undefined T)) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

371 
#> apfst fst) (names ~~ Ts) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

372 
#> (fn (consts, lthy) => 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

373 
let 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

374 
val eqs_t = mk_equations consts 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

375 
val eqs = map (fn eq => Goal.prove lthy argnames [] eq 
42361  376 
(fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t 
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

377 
in 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

378 
fold (fn (name, eq) => Local_Theory.note 
45592  379 
((Binding.conceal 
380 
(Binding.qualify true prfx 

381 
(Binding.qualify true name (Binding.name "simps"))), 

382 
Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd) 

383 
(names ~~ eqs) lthy 

42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

384 
end) 
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset

385 

41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

386 
(** ensuring sort constraints **) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

387 

45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

388 
type instantiation = Datatype.config > Datatype.descr > (string * sort) list 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

389 
> string list > string > string list * string list > typ list * typ list > theory > theory 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

390 

41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

391 
fun perhaps_constrain thy insts raw_vs = 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

392 
let 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

393 
fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

394 
(Logic.varifyT_global T, sort); 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

395 
val vtab = Vartab.empty 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

396 
> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

397 
> fold meet insts; 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

398 
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

399 
end handle Sorts.CLASS_ERROR _ => NONE; 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

400 

45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

401 
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy = 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

402 
let 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

403 
val algebra = Sign.classes_of thy; 
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

404 
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos 
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

405 
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

406 
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd) 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

407 
(Datatype_Aux.interpret_construction descr vs constr) 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

408 
val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] } 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

409 
@ insts_of aux_sort { atyp = K [], dtyp = K o K } 
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

410 
val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos; 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

411 
in if has_inst then thy 
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

412 
else case perhaps_constrain thy insts vs 
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

413 
of SOME constrain => instantiate config descr 
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset

414 
(map constrain vs) tycos prfx (names, auxnames) 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

415 
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

416 
 NONE => thy 
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

417 
end; 
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

418 

473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

419 
fun ensure_common_sort_datatype (sort, instantiate) = 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

420 
ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate)) 
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

421 

473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset

422 
val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

423 

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:
42110
diff
changeset

424 
(** generic parametric compilation **) 
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:
42110
diff
changeset

425 

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:
42110
diff
changeset

426 
fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt 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:
42110
diff
changeset

427 
let 
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:
42110
diff
changeset

428 
val if_t = Const (@{const_name "If"}, @{typ bool} > T > T > T) 
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset

429 
fun mk_if (index, (t, eval_terms)) else_t = if_t $ 
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset

430 
(HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $ 
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:
42110
diff
changeset

431 
(mk_generator_expr ctxt (t, eval_terms)) $ else_t 
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:
42110
diff
changeset

432 
in 
44241  433 
absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) 
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:
42110
diff
changeset

434 
end 
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:
42110
diff
changeset

435 

41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

436 
(** postprocessing of function terms **) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

437 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

438 
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2)) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

439 
 dest_fun_upd t = raise TERM ("dest_fun_upd", [t]) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

440 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

441 
fun mk_fun_upd T1 T2 (t1, t2) t = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

442 
Const (@{const_name fun_upd}, (T1 > T2) > T1 > T2 > T1 > T2) $ t $ t1 $ t2 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

443 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

444 
fun dest_fun_upds t = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

445 
case try dest_fun_upd t of 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

446 
NONE => 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

447 
(case t of 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

448 
Abs (_, _, _) => ([], t) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

449 
 _ => raise TERM ("dest_fun_upds", [t])) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

450 
 SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

451 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

452 
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

453 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

454 
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 > @{typ bool}) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

455 
 make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

456 
 make_set T1 ((t1, @{const True}) :: tps) = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

457 
Const (@{const_name insert}, T1 > (T1 > @{typ bool}) > T1 > @{typ bool}) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

458 
$ t1 $ (make_set T1 tps) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

459 
 make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

460 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

461 
fun make_coset T [] = Const (@{const_abbrev UNIV}, T > @{typ bool}) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

462 
 make_coset T tps = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

463 
let 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

464 
val U = T > @{typ bool} 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

465 
fun invert @{const False} = @{const True} 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

466 
 invert @{const True} = @{const False} 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

467 
in 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

468 
Const (@{const_name "Groups.minus_class.minus"}, U > U > U) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

469 
$ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

470 
end 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

471 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

472 
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 > T2) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

473 
 make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

474 
 make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

475 

d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

476 
fun post_process_term t = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

477 
let 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

478 
fun map_Abs f t = 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

479 
case t of Abs (x, T, t') => Abs (x, T, f t')  _ => raise TERM ("map_Abs", [t]) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

480 
fun process_args t = case strip_comb t of 
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset

481 
(c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

482 
in 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

483 
case fastype_of t of 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

484 
Type (@{type_name fun}, [T1, T2]) => 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

485 
(case try dest_fun_upds t of 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

486 
SOME (tps, t) => 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

487 
(map (pairself post_process_term) tps, map_Abs post_process_term t) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

488 
> (case T2 of 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

489 
@{typ bool} => 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

490 
(case t of 
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset

491 
Abs(_, _, @{const False}) => fst #> rev #> make_set T1 
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset

492 
 Abs(_, _, @{const True}) => fst #> rev #> make_coset T1 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

493 
 Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

494 
 _ => raise TERM ("post_process_term", [t])) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

495 
 Type (@{type_name option}, _) => 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

496 
(case t of 
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset

497 
Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

498 
 Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset

499 
 _ => make_fun_upds T1 T2) 
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

500 
 _ => make_fun_upds T1 T2) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

501 
 NONE => process_args t) 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

502 
 _ => process_args t 
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset

503 
end 
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

504 

8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset

505 
end; 