author  haftmann 
Thu, 15 Nov 2012 17:40:46 +0100  
changeset 50093  a2886be4d615 
parent 50057  57209cfbf16b 
child 51126  df86080de4cb 
permissions  rwrr 
33265  1 
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML 
2 
Author: Lukas Bulwahn, TU Muenchen 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

3 

33265  4 
A quickcheck generator based on the predicate compiler. 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

5 
*) 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

6 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

7 
signature PREDICATE_COMPILE_QUICKCHECK = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

8 
sig 
50057  9 
type seed = Random_Engine.seed 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

10 
(*val quickcheck : Proof.context > term > int > term list option*) 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

11 
val put_pred_result : 
50057  12 
(unit > int > int > int > seed > term list Predicate.pred) > 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

13 
Proof.context > Proof.context; 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

14 
val put_dseq_result : 
50057  15 
(unit > int > int > seed > term list DSequence.dseq * seed) > 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

16 
Proof.context > Proof.context; 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

17 
val put_lseq_result : 
50057  18 
(unit > int > int > seed > int > term list Lazy_Sequence.lazy_sequence) > 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

19 
Proof.context > Proof.context; 
40103  20 
val put_new_dseq_result : (unit > int > term list Lazy_Sequence.lazy_sequence) > 
21 
Proof.context > Proof.context 

45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

22 
val put_cps_result : (unit > int > (bool * term list) option) > 
45450  23 
Proof.context > Proof.context 
24 
val test_goals : (Predicate_Compile_Aux.compilation * bool) > 

43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

25 
Proof.context > bool * bool > (string * typ) list > (term * term list) list 
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

26 
> Quickcheck.result list 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

27 
val nrandom : int Unsynchronized.ref; 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

28 
val debug : bool Unsynchronized.ref; 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

29 
val no_higher_order_predicate : string list Unsynchronized.ref; 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

30 
val setup : theory > theory 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

31 
end; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

32 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

33 
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

34 
struct 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

35 

33257  36 
open Predicate_Compile_Aux; 
37 

50093
a2886be4d615
repaired slip accidentally introduced in 57209cfbf16b
haftmann
parents:
50057
diff
changeset

38 
type seed = Random_Engine.seed; 
50057  39 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

40 
(* FIXME just one data slot (record) per program unit *) 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

41 

f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

42 
structure Pred_Result = Proof_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

43 
( 
50057  44 
type T = unit > int > int > int > seed > term list Predicate.pred 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

45 
(* FIXME avoid user error with nonuser text *) 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

46 
fun init _ () = error "Pred_Result" 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

47 
); 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

48 
val put_pred_result = Pred_Result.put; 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

49 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

50 
structure Dseq_Result = Proof_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

51 
( 
50057  52 
type T = unit > int > int > seed > term list DSequence.dseq * seed 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

53 
(* FIXME avoid user error with nonuser text *) 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

54 
fun init _ () = error "Dseq_Result" 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

55 
); 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

56 
val put_dseq_result = Dseq_Result.put; 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

57 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

58 
structure Lseq_Result = Proof_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

59 
( 
50057  60 
type T = unit > int > int > seed > int > term list Lazy_Sequence.lazy_sequence 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

61 
(* FIXME avoid user error with nonuser text *) 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

62 
fun init _ () = error "Lseq_Result" 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

63 
); 
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

64 
val put_lseq_result = Lseq_Result.put; 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

65 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

66 
structure New_Dseq_Result = Proof_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

67 
( 
40103  68 
type T = unit > int > term list Lazy_Sequence.lazy_sequence 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
40924
diff
changeset

69 
(* FIXME avoid user error with nonuser text *) 
40103  70 
fun init _ () = error "New_Dseq_Random_Result" 
71 
); 

72 
val put_new_dseq_result = New_Dseq_Result.put; 

73 

45450  74 
structure CPS_Result = Proof_Data 
75 
( 

45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

76 
type T = unit > int > (bool * term list) option 
45450  77 
(* FIXME avoid user error with nonuser text *) 
78 
fun init _ () = error "CPS_Result" 

79 
); 

80 
val put_cps_result = CPS_Result.put; 

81 

35537
59dd6be5834c
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
bulwahn
parents:
35380
diff
changeset

82 
val target = "Quickcheck" 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

83 

36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

84 
val nrandom = Unsynchronized.ref 3; 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

85 

35537
59dd6be5834c
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
bulwahn
parents:
35380
diff
changeset

86 
val debug = Unsynchronized.ref false; 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

87 

35538  88 
val no_higher_order_predicate = Unsynchronized.ref ([] : string list); 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

89 

33257  90 
val options = Options { 
91 
expected_modes = NONE, 

39382
c797f3ab2ae1
proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents:
39253
diff
changeset

92 
proposed_modes = [], 
33651
e4aad90618ad
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
bulwahn
parents:
33486
diff
changeset

93 
proposed_names = [], 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

94 
show_steps = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

95 
show_intermediate_results = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

96 
show_proof_trace = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

97 
show_modes = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

98 
show_mode_inference = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

99 
show_compilation = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

100 
show_caught_failures = false, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

101 
show_invalid_clauses = false, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

102 
skip_proof = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

103 
compilation = Random, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

104 
inductify = true, 
36256  105 
specialise = true, 
106 
detect_switches = false, 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

107 
function_flattening = true, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

108 
fail_safe_function_flattening = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

109 
no_higher_order_predicate = [], 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

110 
smart_depth_limiting = true, 
36250  111 
no_topmost_reordering = false 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

112 
} 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

113 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

114 
val debug_options = Options { 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

115 
expected_modes = NONE, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

116 
proposed_modes = [], 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

117 
proposed_names = [], 
33257  118 
show_steps = true, 
119 
show_intermediate_results = true, 

120 
show_proof_trace = false, 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

121 
show_modes = true, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

122 
show_mode_inference = true, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

123 
show_compilation = false, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

124 
show_caught_failures = true, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

125 
show_invalid_clauses = false, 
33257  126 
skip_proof = false, 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

127 
compilation = Random, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

128 
inductify = true, 
36256  129 
specialise = true, 
130 
detect_switches = false, 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

131 
function_flattening = true, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

132 
fail_safe_function_flattening = false, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

133 
no_higher_order_predicate = [], 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

134 
smart_depth_limiting = true, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

135 
no_topmost_reordering = true 
33257  136 
} 
137 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

138 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

139 
fun set_function_flattening b 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

140 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

141 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

142 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

143 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  144 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

145 
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

146 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

147 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

148 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

149 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

150 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  151 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

152 
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

153 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

154 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

155 
fun set_fail_safe_function_flattening b 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

156 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

157 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

158 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

159 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  160 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

161 
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

162 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

163 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

164 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

165 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

166 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  167 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

168 
fail_safe_function_flattening = b, no_higher_order_predicate = no_ho, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

169 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

170 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

171 
fun set_no_higher_order_predicate ss 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

172 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

173 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

174 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

175 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  176 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

177 
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

178 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

179 
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s, 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

180 
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m, 
39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

181 
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, 
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39382
diff
changeset

182 
show_invalid_clauses = s_ic, skip_proof = s_p, 
36256  183 
compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

184 
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, 
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

185 
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

186 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

187 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

188 
fun get_options () = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

189 
set_no_higher_order_predicate (!no_higher_order_predicate) 
45450  190 
(if !debug then debug_options else options) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

191 

45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset

192 
val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns 
45450  193 
val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns 
194 
val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns 

36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

195 

45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset

196 
val mk_randompredT = Predicate_Compile_Aux.mk_monadT RandomPredCompFuns.compfuns 
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36025
diff
changeset

197 
val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns 
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36025
diff
changeset

198 
val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

199 

40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

200 
val mk_new_randompredT = 
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset

201 
Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

202 
val mk_new_return = 
40103  203 
Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

204 
val mk_new_bind = 
40103  205 
Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns 
206 

207 
val mk_new_dseqT = 

45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset

208 
Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns 
40103  209 
val mk_gen_return = 
210 
Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns 

211 
val mk_gen_bind = 

212 
Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns 

213 

36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

214 

45450  215 
val mk_cpsT = 
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset

216 
Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns 
45450  217 
val mk_cps_return = 
218 
Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns 

219 
val mk_cps_bind = 

220 
Predicate_Compile_Aux.mk_bind Pos_Bounded_CPS_Comp_Funs.compfuns 

221 

39756
6c8e83d94536
consolidated tupled_lambda; moved to structure HOLogic
krauss
parents:
39541
diff
changeset

222 
val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

223 

42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset

224 
fun cpu_time description e = 
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset

225 
let val ({cpu, ...}, result) = Timing.timing e () 
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset

226 
in (result, (description, Time.toMilliseconds cpu)) end 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

227 

43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

228 
fun compile_term compilation options ctxt t = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

229 
let 
44241  230 
val t' = fold_rev absfree (Term.add_frees t []) t 
42361  231 
val thy = Theory.copy (Proof_Context.theory_of ctxt) 
39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39471
diff
changeset

232 
val ((((full_constname, constT), vs'), intro), thy1) = 
42031  233 
Predicate_Compile_Aux.define_quickcheck_predicate t' thy 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

234 
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 
36256  235 
val (thy3, preproc_time) = cpu_time "predicate preprocessing" 
39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39471
diff
changeset

236 
(fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

237 
val (thy4, core_comp_time) = cpu_time "random_dseq core compilation" 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

238 
(fn () => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

239 
case compilation of 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

240 
Pos_Random_DSeq => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

241 
Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

242 
 New_Pos_Random_DSeq => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

243 
Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3 
40103  244 
 Pos_Generator_DSeq => 
245 
Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3 

45450  246 
 Pos_Generator_CPS => 
247 
Predicate_Compile_Core.add_generator_cps_equations options [full_constname] thy3 

36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

248 
(* Depth_Limited_Random => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

249 
Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*)) 
36256  250 
(*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*) 
42361  251 
val ctxt4 = Proof_Context.init_global thy4 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

252 
val modes = Core_Data.modes_of compilation ctxt4 full_constname 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

253 
val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

254 
val prog = 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

255 
if member eq_mode modes output_mode then 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

256 
let 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39756
diff
changeset

257 
val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

258 
val T = 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

259 
case compilation of 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

260 
Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs')) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

261 
 New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs')) 
40103  262 
 Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs')) 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

263 
 Depth_Limited_Random => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

264 
[@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral}, 
50057  265 
@{typ Random.seed}] > mk_predT (HOLogic.mk_tupleT (map snd vs')) 
45450  266 
 Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs')) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

267 
in 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

268 
Const (name, T) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34028
diff
changeset

269 
end 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

270 
else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes)) 
45450  271 
fun mk_Some T = Const (@{const_name "Option.Some"}, T > Type (@{type_name "Option.option"}, [T])) 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

272 
val qc_term = 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

273 
case compilation of 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

274 
Pos_Random_DSeq => mk_bind (prog, 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

275 
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

276 
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

277 
 New_Pos_Random_DSeq => mk_new_bind (prog, 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

278 
mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term} 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

279 
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) 
40103  280 
 Pos_Generator_DSeq => mk_gen_bind (prog, 
281 
mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term} 

282 
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) 

45450  283 
 Pos_Generator_CPS => prog $ 
45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

284 
mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $ 
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

285 
HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term} 
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

286 
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))) 
44241  287 
 Depth_Limited_Random => fold_rev absdummy 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

288 
[@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral}, 
50057  289 
@{typ Random.seed}] 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

290 
(mk_bind' (list_comb (prog, map Bound (3 downto 0)), 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

291 
mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term} 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

292 
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

293 
val prog = 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

294 
case compilation of 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

295 
Pos_Random_DSeq => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

296 
let 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

297 
val compiled_term = 
39471  298 
Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result") 
299 
thy4 (SOME target) 

36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

300 
(fn proc => fn g => fn n => fn size => fn s => g n size s >> (DSequence.map o map) proc) 
39471  301 
qc_term [] 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

302 
in 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

303 
(fn size => fn nrandom => fn depth => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

304 
Option.map fst (DSequence.yield 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

305 
(compiled_term nrandom size > Random_Engine.run) depth true)) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

306 
end 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

307 
 New_Pos_Random_DSeq => 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

308 
let 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

309 
val compiled_term = 
39471  310 
Code_Runtime.dynamic_value_strict 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

311 
(Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result") 
39471  312 
thy4 (SOME target) 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

313 
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => 
36533  314 
g nrandom size s depth > (Lazy_Sequence.mapa o map) proc) 
39471  315 
qc_term [] 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

316 
in 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

317 
fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

318 
( 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

319 
let 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

320 
val seed = Random_Engine.next_seed () 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

321 
in compiled_term nrandom size seed depth end)) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

322 
end 
40103  323 
 Pos_Generator_DSeq => 
324 
let 

325 
val compiled_term = 

326 
Code_Runtime.dynamic_value_strict 

327 
(New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result") 

328 
thy4 (SOME target) 

329 
(fn proc => fn g => fn depth => g depth > (Lazy_Sequence.mapa o map) proc) 

330 
qc_term [] 

331 
in 

332 
fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth)) 

333 
end 

45450  334 
 Pos_Generator_CPS => 
335 
let 

336 
val compiled_term = 

337 
Code_Runtime.dynamic_value_strict 

338 
(CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result") 

339 
thy4 (SOME target) 

45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

340 
(fn proc => fn g => fn depth => g depth > Option.map (apsnd (map proc))) 
45450  341 
qc_term [] 
342 
in 

45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

343 
fn size => fn nrandom => Option.map snd o compiled_term 
45450  344 
end 
40103  345 
 Depth_Limited_Random => 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

346 
let 
39471  347 
val compiled_term = Code_Runtime.dynamic_value_strict 
39388
fdbb2c55ffc2
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references
haftmann
parents:
39253
diff
changeset

348 
(Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result") 
39471  349 
thy4 (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed => 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

350 
g depth nrandom size seed > (Predicate.map o map) proc) 
39471  351 
qc_term [] 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

352 
in 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

353 
fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

354 
(compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s))))) 
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

355 
end 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

356 
in 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

357 
prog 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

358 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

359 

45214  360 
fun try_upto_depth ctxt f = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

361 
let 
45214  362 
val max_depth = Config.get ctxt Quickcheck.depth 
363 
fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s 

364 
fun try' i = 

365 
if i <= max_depth then 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

366 
let 
45214  367 
val _ = message ("Depth: " ^ string_of_int i) 
368 
val (result, time) = 

369 
cpu_time ("Depth " ^ string_of_int i) (fn () => 

370 
f i handle Match => (if Config.get ctxt Quickcheck.quiet then () 

371 
else warning "Exception Match raised during quickcheck"; NONE)) 

372 
val _ = if Config.get ctxt Quickcheck.timing then 

373 
message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else () 

35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

374 
in 
45214  375 
case result of NONE => try' (i + 1)  SOME q => SOME q 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

376 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

377 
else 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

378 
NONE 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

379 
in 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

380 
try' 0 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

381 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

382 

c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

383 
(* quickcheck interface functions *) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

384 

45214  385 
fun compile_term' compilation options ctxt (t, eval_terms) = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

386 
let 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

387 
val size = Config.get ctxt Quickcheck.size 
36025
d25043e7843f
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents:
35886
diff
changeset

388 
val c = compile_term compilation options ctxt t 
45214  389 
val counterexample = try_upto_depth ctxt (c size (!nrandom)) 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

390 
in 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

391 
Quickcheck.Result 
45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45484
diff
changeset

392 
{counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample, 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

393 
evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

394 
end 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

395 

45214  396 
fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening = 
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

397 
let 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

398 
val options = 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

399 
set_fail_safe_function_flattening fail_safe_function_flattening 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

400 
(set_function_flattening function_flattening (get_options ())) 
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset

401 
in 
45214  402 
compile_term' compilation options 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

403 
end 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

404 

43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

405 

45450  406 
fun test_goals options ctxt catch_code_errors insts goals = 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

407 
let 
45450  408 
val (compilation, fail_safe_function_flattening) = options 
409 
val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion) 

45214  410 
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

411 
val test_term = 
45214  412 
quickcheck_compile_term compilation function_flattening fail_safe_function_flattening 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

413 
in 
45214  414 
Quickcheck_Common.collect_results (test_term ctxt) 
43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

415 
(maps (map snd) correct_inst_goals) [] 
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

416 
end 
45450  417 

418 
val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true); 

419 
val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false); 

43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

420 

45484
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45461
diff
changeset

421 
val setup = 
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45461
diff
changeset

422 
Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
23871e17dddb
setting up exhaustive generators which are used for the smart generators
bulwahn
parents:
45461
diff
changeset

423 
#> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive", 
45450  424 
(smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false)))) 
425 
#> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive", 

426 
(smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false)))) 

43886
bf068e758783
adapting quickcheck based on the analysis of the predicate compiler
bulwahn
parents:
42361
diff
changeset

427 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset

428 
end; 