src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
author haftmann
Thu, 15 Nov 2012 17:40:46 +0100
changeset 50093 a2886be4d615
parent 50057 57209cfbf16b
child 51126 df86080de4cb
permissions -rw-r--r--
repaired slip accidentally introduced in 57209cfbf16b
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33257
diff changeset
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
01c9c6dbd890 proper headers;
wenzelm
parents: 33257
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     3
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33257
diff changeset
     4
A quickcheck generator based on the predicate compiler.
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     5
*)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     6
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     7
signature PREDICATE_COMPILE_QUICKCHECK =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     8
sig
50057
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
     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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    20
  val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    23
    Proof.context -> Proof.context
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    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 HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    31
end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    32
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    33
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    34
struct
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    35
33257
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
    36
open Predicate_Compile_Aux;
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
    37
50093
a2886be4d615 repaired slip accidentally introduced in 57209cfbf16b
haftmann
parents: 50057
diff changeset
    38
type seed = Random_Engine.seed;
50057
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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 non-user 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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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 non-user 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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
    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 non-user 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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    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 non-user text *)
40103
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    70
  fun init _ () = error "New_Dseq_Random_Result"
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    71
);
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    72
val put_new_dseq_result = New_Dseq_Result.put;
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
    73
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    74
structure CPS_Result = Proof_Data
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    77
  (* FIXME avoid user error with non-user text *)
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    78
  fun init _ () = error "CPS_Result"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    79
);
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    80
val put_cps_result = CPS_Result.put;
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    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
94170181a842 made smlnj happy
bulwahn
parents: 35537
diff changeset
    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
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
    90
val options = Options {
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
    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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   105
  specialise = true,
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
ad558b642a15 switched off no_topmost_reordering
bulwahn
parents: 36046
diff changeset
   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
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   118
  show_steps = true,
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   119
  show_intermediate_results = true,
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   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
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   129
  specialise = true,
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   136
}
95186fb5653c added examples for quickcheck prototype
bulwahn
parents: 33256
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   193
val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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 HOL-Main; 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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   205
  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   206
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   209
val mk_gen_return =
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   210
  Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   211
val mk_gen_bind =
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   212
  Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   213
  
36025
d25043e7843f made quickcheck generic with respect to which compilation; added random compilation to quickcheck
bulwahn
parents: 35886
diff changeset
   214
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   217
val mk_cps_return =
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   218
  Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   219
val mk_cps_bind =
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   220
  Predicate_Compile_Aux.mk_bind Pos_Bounded_CPS_Comp_Funs.compfuns
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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 HOL-Main; 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
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43886
diff changeset
   230
    val t' = fold_rev absfree (Term.add_frees t []) t
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42159
diff changeset
   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
2de57cda5b24 adapting predicate_compile_quickcheck; tuned
bulwahn
parents: 41472
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   244
          | Pos_Generator_DSeq =>
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   245
              Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   246
          | Pos_Generator_CPS =>
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
d1d9dee7a4bf adopting quickcheck
bulwahn
parents: 36250
diff changeset
   250
    (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42159
diff changeset
   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 HOL-Main; 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 HOL-Main; 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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
   265
              @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   280
        | Pos_Generator_DSeq => mk_gen_bind (prog,
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   281
            mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   282
            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43886
diff changeset
   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
57209cfbf16b prefer explicit Random.seed
haftmann
parents: 45750
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   298
              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
f8df589ca2a5 dropped unnecessary ML code
haftmann
parents: 36256
diff changeset
   314
                  g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
39471
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   323
      | Pos_Generator_DSeq =>
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   324
          let
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   325
            val compiled_term =
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   326
              Code_Runtime.dynamic_value_strict
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   327
                (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   328
                thy4 (SOME target)
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   329
                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.mapa o map) proc)
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   330
                qc_term []
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   331
          in
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   332
            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   333
          end
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   334
      | Pos_Generator_CPS =>
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   335
          let
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   336
            val compiled_term =
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   337
              Code_Runtime.dynamic_value_strict
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   338
                (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   341
                qc_term []
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   344
          end
40103
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40054
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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
55e0ff582fa4 adjusted to changes in Code_Runtime
haftmann
parents: 39403
diff changeset
   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 HOL-Main; 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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   362
    val max_depth = Config.get ctxt Quickcheck.depth
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   363
    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   364
    fun try' i =
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   367
          val _ = message ("Depth: " ^ string_of_int i)
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   368
          val (result, time) =
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   369
            cpu_time ("Depth " ^ string_of_int i) (fn () =>
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   370
              f i handle Match => (if Config.get ctxt Quickcheck.quiet then ()
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   371
                    else warning "Exception Match raised during quickcheck"; NONE))
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   372
         val _ = if Config.get ctxt Quickcheck.timing then
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   402
    compile_term' compilation options
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   403
  end
5c2af18a3237 including the predicate compiler in HOL-Main; 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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   408
    val (compilation, fail_safe_function_flattening) = options
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   409
    val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion)
45214
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   417
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   418
val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   424
    (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   425
  #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   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 HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   428
end;