src/HOL/Tools/Quickcheck/exhaustive_generators.ML
author wenzelm
Thu, 14 Apr 2016 15:56:30 +0200
changeset 62981 3a01f1f58630
parent 62979 1e527c40ae40
child 67149 e61557884799
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41923
f05fc0711bc7 renaming signatures and structures; correcting header
bulwahn
parents: 41920
diff changeset
     1
(*  Title:      HOL/Tools/Quickcheck/exhaustive_generators.ML
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     3
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41917
diff changeset
     4
Exhaustive generators for various types.
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     5
*)
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     6
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41917
diff changeset
     7
signature EXHAUSTIVE_GENERATORS =
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     8
sig
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
     9
  val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    10
    (bool * term list) option * Quickcheck.report option
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42028
diff changeset
    11
  val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
    12
  val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    13
  val put_counterexample:
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    14
    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    15
      Proof.context -> Proof.context
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    16
  val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list) ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    17
    Proof.context -> Proof.context
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    18
  val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    19
    Proof.context -> Proof.context
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    20
  exception Counterexample of term list
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
    21
  val smart_quantifier : bool Config.T
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
    22
  val optimise_equality : bool Config.T
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
    23
  val quickcheck_pretty : bool Config.T
45484
23871e17dddb setting up exhaustive generators which are used for the smart generators
bulwahn
parents: 45420
diff changeset
    24
  val setup_exhaustive_datatype_interpretation : theory -> theory
48178
0192811f0a96 exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents: 48013
diff changeset
    25
  val setup_bounded_forall_datatype_interpretation : theory -> theory
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
    26
  val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    27
    (string * sort) list -> string list -> string -> string list * string list ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    28
    typ list * typ list -> theory -> theory
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
    29
  val instantiate_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    30
    (string * sort) list -> string list -> string -> string list * string list ->
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    31
    typ list * typ list -> theory -> theory
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    32
end
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    33
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41917
diff changeset
    34
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    35
struct
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    36
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    37
(* basics *)
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    38
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    39
(** dynamic options **)
40907
45ba9f05583a adding smart quantifiers to exhaustive testing
bulwahn
parents: 40901
diff changeset
    40
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42391
diff changeset
    41
val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
    42
val optimise_equality = Attrib.setup_config_bool @{binding quickcheck_optimise_equality} (K true)
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
    43
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42391
diff changeset
    44
val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42391
diff changeset
    45
val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42391
diff changeset
    46
val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42391
diff changeset
    47
val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    48
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    49
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    50
(** abstract syntax **)
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    51
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    52
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"})
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40420
diff changeset
    53
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    54
val size = @{term "i :: natural"}
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    55
val size_pred = @{term "(i :: natural) - 1"}
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    56
val size_ge_zero = @{term "(i :: natural) > 0"}
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
    57
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    58
fun mk_none_continuation (x, y) =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    59
  let val (T as Type (@{type_name option}, _)) = fastype_of x
62981
wenzelm
parents: 62979
diff changeset
    60
  in Const (@{const_name orelse}, T --> T --> T) $ x $ y end
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    61
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45718
diff changeset
    62
fun mk_if (b, t, e) =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    63
  let val T = fastype_of t
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    64
  in Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    65
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45718
diff changeset
    66
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    67
(* handling inductive datatypes *)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    68
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    69
(** constructing generator instances **)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    70
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    71
exception FUNCTION_TYPE
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    72
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    73
exception Counterexample of term list
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    74
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    75
val resultT =  @{typ "(bool * term list) option"}
45722
63b42a7db003 changing the exhaustive generator signatures;
bulwahn
parents: 45721
diff changeset
    76
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    77
val exhaustiveN = "exhaustive"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    78
val full_exhaustiveN = "full_exhaustive"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    79
val bounded_forallN = "bounded_forall"
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    80
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
    81
fun fast_exhaustiveT T = (T --> @{typ unit}) --> @{typ natural} --> @{typ unit}
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
    82
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    83
fun exhaustiveT T = (T --> resultT) --> @{typ natural} --> resultT
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
    84
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    85
fun bounded_forallT T = (T --> @{typ bool}) --> @{typ natural} --> @{typ bool}
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
    86
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    87
fun full_exhaustiveT T = (termifyT T --> resultT) --> @{typ natural} --> resultT
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40913
diff changeset
    88
45722
63b42a7db003 changing the exhaustive generator signatures;
bulwahn
parents: 45721
diff changeset
    89
fun check_allT T = (termifyT T --> resultT) --> resultT
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40913
diff changeset
    90
42307
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    91
fun mk_equation_terms generics (descr, vs, Ts) =
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    92
  let
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    93
    val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    94
    val rhss =
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
    95
      Old_Datatype_Aux.interpret_construction descr vs
42307
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    96
        { atyp = mk_call, dtyp = mk_aux_call }
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    97
      |> (map o apfst) Type
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    98
      |> map (fn (T, cs) => map (mk_consexpr T) cs)
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
    99
      |> map mk_rhs
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
   100
    val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   101
  in map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) end
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   102
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43878
diff changeset
   103
fun gen_mk_call c T =  (T, fn t => c T $ absdummy T t $ size_pred)
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   104
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   105
fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   106
  let
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   107
    val T = Type (tyco, Ts)
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   108
    val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   109
  in (T, fn t => nth functerms k $ absdummy T t $ size_pred) end
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   110
46306
bulwahn
parents: 46042
diff changeset
   111
fun gen_mk_consexpr test_function simpleT (c, xs) =
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   112
  let
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   113
    val (Ts, fns) = split_list xs
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   114
    val constr = Const (c, Ts ---> simpleT)
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   115
    val bounds = map Bound (((length xs) - 1) downto 0)
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   116
    val start_term = test_function simpleT $ list_comb (constr, bounds)
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   117
  in fold_rev (fn f => fn t => f t) fns start_term end
42307
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
   118
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
   119
fun mk_equations functerms =
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   120
  let
45724
1f5fc44254d7 the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn
parents: 45722
diff changeset
   121
    fun test_function T = Free ("f", T --> resultT)
62981
wenzelm
parents: 62979
diff changeset
   122
    val mk_call = gen_mk_call (fn T => Const (@{const_name exhaustive}, exhaustiveT T))
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   123
    val mk_aux_call = gen_mk_aux_call functerms
46306
bulwahn
parents: 46042
diff changeset
   124
    val mk_consexpr = gen_mk_consexpr test_function
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   125
    fun mk_rhs exprs =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   126
      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   127
  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   128
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   129
fun mk_bounded_forall_equations functerms =
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   130
  let
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   131
    fun test_function T = Free ("P", T --> @{typ bool})
62981
wenzelm
parents: 62979
diff changeset
   132
    val mk_call = gen_mk_call (fn T => Const (@{const_name bounded_forall}, bounded_forallT T))
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   133
    val mk_aux_call = gen_mk_aux_call functerms
46306
bulwahn
parents: 46042
diff changeset
   134
    val mk_consexpr = gen_mk_consexpr test_function
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   135
    fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True})
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   136
  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   137
42307
72e2fabb4bc2 creating a general mk_equation_terms for the different compilations
bulwahn
parents: 42306
diff changeset
   138
fun mk_full_equations functerms =
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   139
  let
45722
63b42a7db003 changing the exhaustive generator signatures;
bulwahn
parents: 45721
diff changeset
   140
    fun test_function T = Free ("f", termifyT T --> resultT)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   141
    fun case_prod_const T =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   142
      HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT)
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   143
    fun mk_call T =
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   144
      let
62981
wenzelm
parents: 62979
diff changeset
   145
        val full_exhaustive = Const (@{const_name full_exhaustive}, full_exhaustiveT T)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   146
      in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   147
        (T,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   148
          fn t =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   149
            full_exhaustive $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   150
              (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   151
              size_pred)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   152
      end
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41917
diff changeset
   153
    fun mk_aux_call fTs (k, _) (tyco, Ts) =
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   154
      let
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   155
        val T = Type (tyco, Ts)
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   156
        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   157
      in
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   158
        (T,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   159
          fn t =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   160
            nth functerms k $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   161
              (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   162
              size_pred)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   163
      end
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   164
    fun mk_consexpr simpleT (c, xs) =
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   165
      let
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   166
        val (Ts, fns) = split_list xs
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   167
        val constr = Const (c, Ts ---> simpleT)
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40420
diff changeset
   168
        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 56241
diff changeset
   169
        val Eval_App =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   170
          Const (@{const_name Code_Evaluation.App},
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   171
            HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 56241
diff changeset
   172
        val Eval_Const =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   173
          Const (@{const_name Code_Evaluation.Const},
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   174
            HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   175
        val term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   176
          fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   177
            bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   178
        val start_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   179
          test_function simpleT $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   180
            (HOLogic.pair_const simpleT @{typ "unit \<Rightarrow> Code_Evaluation.term"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   181
              (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   182
      in fold_rev (fn f => fn t => f t) fns start_term end
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   183
    fun mk_rhs exprs =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   184
      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   185
  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   186
40901
8fdfa9c4e7ed smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents: 40899
diff changeset
   187
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   188
(** instantiating generator classes **)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   189
42325
104472645443 made SML/NJ happy;
wenzelm
parents: 42316
diff changeset
   190
fun contains_recursive_type_under_function_types xs =
42312
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   191
  exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
   192
    (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   193
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   194
fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   195
    config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
42312
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   196
  if not (contains_recursive_type_under_function_types descr) then
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   197
    let
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
   198
      val _ = Old_Datatype_Aux.message config ("Creating " ^ name ^ "...")
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   199
      val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames)
42312
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   200
    in
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   201
      thy
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   202
      |> Class.instantiation (tycos, vs, sort)
42312
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   203
      |> Quickcheck_Common.define_functions
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   204
          (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE)
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   205
          prfx argnames fullnames (map mk_T (Ts @ Us))
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59154
diff changeset
   206
      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
42312
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   207
    end
5bf3b9612e43 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
bulwahn
parents: 42310
diff changeset
   208
  else
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57996
diff changeset
   209
    (Old_Datatype_Aux.message config
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   210
      ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
42230
594480d25aaa deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents: 42229
diff changeset
   211
    thy)
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   212
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   213
val instantiate_bounded_forall_datatype =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   214
  instantiate_datatype
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   215
    ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   216
      mk_bounded_forall_equations, bounded_forallT, ["P", "i"])
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   217
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   218
val instantiate_exhaustive_datatype =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   219
  instantiate_datatype
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   220
    ("exhaustive generators", exhaustiveN, @{sort exhaustive},
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   221
      mk_equations, exhaustiveT, ["f", "i"])
42315
95dfa082065a generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
bulwahn
parents: 42314
diff changeset
   222
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   223
val instantiate_full_exhaustive_datatype =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   224
  instantiate_datatype
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   225
    ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   226
      mk_full_equations, full_exhaustiveT, ["f", "i"])
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   227
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   228
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   229
(* building and compiling generator expressions *)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   230
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   231
fun mk_let_expr (x, t, e) genuine =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   232
  let val (T1, T2) = (fastype_of x, fastype_of (e genuine))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   233
  in Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) end
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   234
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   235
fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine =
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   236
  let
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   237
    val (T1, T2) = (fastype_of x, fastype_of (e genuine))
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   238
    val if_t = Const (@{const_name If}, @{typ bool} --> T2 --> T2 --> T2)
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   239
  in
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   240
    Const (@{const_name Quickcheck_Random.catch_match}, T2 --> T2 --> T2) $
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   241
      (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   242
      (if_t $ genuine_only $ none $ safe false)
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   243
  end
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   244
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   245
fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt =
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   246
  let
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   247
    val cnstrs =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   248
      flat (maps
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   249
        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   250
        (Symtab.dest
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   251
          (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs)))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   252
    fun is_constrt (Const (s, T), ts) =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   253
          (case (AList.lookup (op =) cnstrs s, body_type T) of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   254
            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   255
          | _ => false)
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   256
      | is_constrt _ = false
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   257
    fun mk_naive_test_term t =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   258
      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true)
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   259
    fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45718
diff changeset
   260
    fun mk_smart_test_term' concl bound_vars assms genuine =
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   261
      let
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   262
        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   263
        fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   264
              if member (op =) (Term.add_free_names lhs bound_vars) x then
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   265
                c (assm, assms)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   266
              else
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   267
                let
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   268
                   val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   269
                   fun safe genuine =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   270
                     the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   271
                in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   272
                  mk_test (remove (op =) x (vars_of assm),
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   273
                    mk_let safe f (try lookup x) lhs
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   274
                      (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   275
    
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   276
                end
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   277
          | mk_equality_term (lhs, t) c (assm, assms) =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   278
              if is_constrt (strip_comb t) then
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   279
                let
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   280
                  val (constr, args) = strip_comb t
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   281
                  val T = fastype_of t
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   282
                  val vars =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   283
                    map Free
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   284
                      (Variable.variant_frees ctxt (concl :: assms)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   285
                        (map (fn t => ("x", fastype_of t)) args))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   286
                  val varnames = map (fst o dest_Free) vars
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   287
                  val dummy_var =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   288
                    Free (singleton
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   289
                      (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   290
                  val new_assms = map HOLogic.mk_eq (vars ~~ args)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   291
                  val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   292
                  val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   293
                in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   294
                  mk_test (vars_of lhs,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   295
                    Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   296
                      [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   297
                end
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   298
              else c (assm, assms)
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   299
        fun default (assm, assms) =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   300
          mk_test
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   301
            (vars_of assm,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   302
              mk_if (HOLogic.mk_not assm, none_t,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   303
                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   304
      in
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   305
        (case assms of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   306
          [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   307
        | assm :: assms =>
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   308
            if Config.get ctxt optimise_equality then
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   309
              (case try HOLogic.dest_eq assm of
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   310
                SOME (lhs, rhs) =>
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   311
                  mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms)
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   312
              | NONE => default (assm, assms))
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   313
            else default (assm, assms))
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   314
      end
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   315
    val mk_smart_test_term =
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45718
diff changeset
   316
      Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   317
  in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   318
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   319
fun mk_fast_generator_expr ctxt (t, eval_terms) =
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   320
  let
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   321
    val ctxt' = Variable.auto_fixes t ctxt
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   322
    val names = Term.add_free_names t []
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   323
    val frees = map Free (Term.add_frees t [])
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   324
    fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
46306
bulwahn
parents: 46042
diff changeset
   325
    val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   326
    val depth = Free (depth_name, @{typ natural})
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   327
    fun return _ =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   328
      @{term "throw_Counterexample :: term list \<Rightarrow> unit"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   329
        (HOLogic.mk_list @{typ term}
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   330
          (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   331
    fun mk_exhaustive_closure (free as Free (_, T)) t =
62981
wenzelm
parents: 62979
diff changeset
   332
      Const (@{const_name fast_exhaustive}, fast_exhaustiveT T) $ lambda free t $ depth
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   333
    val none_t = @{term "()"}
45761
90028fd2f1fa exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents: 45754
diff changeset
   334
    fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   335
    fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   336
    val mk_test_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   337
      mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   338
  in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   339
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   340
fun mk_unknown_term T =
62981
wenzelm
parents: 62979
diff changeset
   341
  HOLogic.reflect_term (Const (@{const_name unknown}, T))
45688
d4ac5e090cd9 also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents: 45684
diff changeset
   342
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   343
fun mk_safe_term t =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   344
  @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   345
    (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)
45688
d4ac5e090cd9 also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents: 45684
diff changeset
   346
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   347
fun mk_return t genuine =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   348
  @{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   349
    (HOLogic.pair_const @{typ bool} @{typ "term list"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   350
      Quickcheck_Common.reflect_bool genuine $ t)
45724
1f5fc44254d7 the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn
parents: 45722
diff changeset
   351
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   352
fun mk_generator_expr ctxt (t, eval_terms) =
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   353
  let
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   354
    val ctxt' = Variable.auto_fixes t ctxt
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   355
    val names = Term.add_free_names t []
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   356
    val frees = map Free (Term.add_frees t [])
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   357
    fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
46306
bulwahn
parents: 46042
diff changeset
   358
    val ([depth_name, genuine_only_name], _) =
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   359
      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   360
    val depth = Free (depth_name, @{typ natural})
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   361
    val genuine_only = Free (genuine_only_name, @{typ bool})
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   362
    val return =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   363
      mk_return (HOLogic.mk_list @{typ term}
45688
d4ac5e090cd9 also potential counterexamples in the simple exhaustive testing in quickcheck
bulwahn
parents: 45684
diff changeset
   364
        (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   365
    fun mk_exhaustive_closure (free as Free (_, T)) t =
62981
wenzelm
parents: 62979
diff changeset
   366
      Const (@{const_name exhaustive}, exhaustiveT T) $ lambda free t $ depth
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   367
    val none_t = Const (@{const_name None}, resultT)
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
   368
    val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   369
    fun mk_let safe def v_opt t e =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   370
      mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   371
    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   372
  in lambda genuine_only (lambda depth (mk_test_term t)) end
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   373
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   374
fun mk_full_generator_expr ctxt (t, eval_terms) =
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   375
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42325
diff changeset
   376
    val thy = Proof_Context.theory_of ctxt
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   377
    val ctxt' = Variable.auto_fixes t ctxt
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   378
    val names = Term.add_free_names t []
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   379
    val frees = map Free (Term.add_frees t [])
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45732
diff changeset
   380
    val ([depth_name, genuine_only_name], ctxt'') =
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45732
diff changeset
   381
      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
46306
bulwahn
parents: 46042
diff changeset
   382
    val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt''
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   383
    val depth = Free (depth_name, @{typ natural})
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   384
    val genuine_only = Free (genuine_only_name, @{typ bool})
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   385
    val term_vars = map (fn n => Free (n, @{typ "unit \<Rightarrow> term"})) term_names
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   386
    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   387
    val return =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   388
      mk_return
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   389
        (HOLogic.mk_list @{typ term}
45724
1f5fc44254d7 the simple exhaustive compilation also indicates if counterexample is potentially spurious;
bulwahn
parents: 45722
diff changeset
   390
          (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   391
    fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
46331
f5598b604a54 generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents: 46306
diff changeset
   392
      if Sign.of_sort thy (T, @{sort check_all}) then
62981
wenzelm
parents: 62979
diff changeset
   393
        Const (@{const_name check_all}, check_allT T) $
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   394
          (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   395
            lambda free (lambda term_var t))
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   396
      else
62981
wenzelm
parents: 62979
diff changeset
   397
        Const (@{const_name full_exhaustive}, full_exhaustiveT T) $
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   398
          (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   399
            lambda free (lambda term_var t)) $ depth
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   400
    val none_t = Const (@{const_name None}, resultT)
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
   401
    val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   402
    fun mk_let safe _ (SOME (v, term_var)) t e =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   403
          mk_safe_let_expr genuine_only none_t safe (v, t,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   404
            e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))])
48414
43875bab3a4c handling partiality in the case where the equality optimisation is applied
bulwahn
parents: 48273
diff changeset
   405
      | mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e)
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   406
    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45732
diff changeset
   407
  in lambda genuine_only (lambda depth (mk_test_term t)) end
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   408
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42273
diff changeset
   409
fun mk_parametric_generator_expr mk_generator_expr =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   410
  Quickcheck_Common.gen_mk_parametric_generator_expr
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   411
    ((mk_generator_expr,
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   412
      absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))),
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   413
      @{typ bool} --> @{typ natural} --> resultT)
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   414
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   415
fun mk_validator_expr ctxt t =
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   416
  let
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   417
    fun bounded_forallT T = (T --> @{typ bool}) --> @{typ natural} --> @{typ bool}
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   418
    val ctxt' = Variable.auto_fixes t ctxt
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   419
    val names = Term.add_free_names t []
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   420
    val frees = map Free (Term.add_frees t [])
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   421
    fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
46306
bulwahn
parents: 46042
diff changeset
   422
    val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   423
    val depth = Free (depth_name, @{typ natural})
42390
be7af468f7b3 creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
bulwahn
parents: 42361
diff changeset
   424
    fun mk_bounded_forall (Free (s, T)) t =
62981
wenzelm
parents: 62979
diff changeset
   425
      Const (@{const_name bounded_forall}, bounded_forallT T) $ lambda (Free (s, T)) t $ depth
45761
90028fd2f1fa exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents: 45754
diff changeset
   426
    fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
50046
0051dc4f301f dropped dead code;
haftmann
parents: 48414
diff changeset
   427
    fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45718
diff changeset
   428
    val mk_test_term =
48013
44de84112a67 added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents: 46565
diff changeset
   429
      mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   430
  in lambda depth (mk_test_term t) end
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   431
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   432
fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) =
42391
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   433
  let
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   434
    val frees = Term.add_free_names t []
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   435
    val dummy_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   436
      @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"}
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   437
    val return =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   438
      @{term "Some :: term list => term list option"} $
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   439
        (HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term))
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43878
diff changeset
   440
    val wrap = absdummy @{typ bool}
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   441
      (@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43878
diff changeset
   442
        Bound 0 $ @{term "None :: term list option"} $ return)
42391
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   443
  in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   444
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   445
42028
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   446
(** generator compiliation **)
bd6515e113b2 passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents: 42027
diff changeset
   447
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   448
structure Data = Proof_Data
41861
77d87dc50e5a adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents: 41472
diff changeset
   449
(
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   450
  type T =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   451
    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) *
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   452
    (unit -> (Code_Numeral.natural -> term list option) list) *
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   453
    (unit -> (Code_Numeral.natural -> bool) list)
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   454
  val empty: T =
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   455
   (fn () => raise Fail "counterexample",
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   456
    fn () => raise Fail "counterexample_batch",
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   457
    fn () => raise Fail "validator_batch")
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   458
  fun init _ = empty
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   459
)
41861
77d87dc50e5a adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents: 41472
diff changeset
   460
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   461
val get_counterexample = #1 o Data.get
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   462
val get_counterexample_batch = #2 o Data.get
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   463
val get_validator_batch = #3 o Data.get
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   464
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   465
val put_counterexample = Data.map o @{apply 3(1)} o K
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   466
val put_counterexample_batch = Data.map o @{apply 3(2)} o K
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   467
val put_validator_batch = Data.map o @{apply 3(3)} o K
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   468
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   469
val target = "Quickcheck"
42391
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   470
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   471
fun compile_generator_expr_raw ctxt ts =
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42028
diff changeset
   472
  let
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   473
    val mk_generator_expr =
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   474
      if Config.get ctxt fast then mk_fast_generator_expr
42391
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   475
      else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
42306
51a08b2699d5 adding an even faster compilation scheme
bulwahn
parents: 42304
diff changeset
   476
      else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   477
    val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   478
    val compile =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   479
      Code_Runtime.dynamic_value_strict
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   480
        (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   481
        ctxt (SOME target)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   482
        (fn proc => fn g => fn card => fn genuine_only => fn size =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   483
          g card genuine_only size
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   484
          |> (Option.map o apsnd o map) proc) t' []
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42028
diff changeset
   485
  in
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   486
    fn genuine_only => fn [card, size] =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   487
      rpair NONE (compile card genuine_only size
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   488
      |> (if Config.get ctxt quickcheck_pretty then
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   489
          Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   490
  end
42391
d7b58dc35cc5 adding bounded_forall tester
bulwahn
parents: 42390
diff changeset
   491
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   492
fun compile_generator_expr ctxt ts =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   493
  let val compiled = compile_generator_expr_raw ctxt ts in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   494
    fn genuine_only => fn [card, size] =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   495
      compiled genuine_only
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   496
        [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   497
  end
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   498
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   499
fun compile_generator_exprs_raw ctxt ts =
41861
77d87dc50e5a adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents: 41472
diff changeset
   500
  let
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   501
    val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   502
    val compiles =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   503
      Code_Runtime.dynamic_value_strict
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   504
        (get_counterexample_batch, put_counterexample_batch,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   505
          "Exhaustive_Generators.put_counterexample_batch")
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   506
        ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   507
        (HOLogic.mk_list @{typ "natural => term list option"} ts') []
41861
77d87dc50e5a adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents: 41472
diff changeset
   508
  in
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   509
    map (fn compile => fn size =>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   510
      compile size |> (Option.map o map) Quickcheck_Common.post_process_term) compiles
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   511
  end
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   512
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   513
fun compile_generator_exprs ctxt ts =
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   514
  compile_generator_exprs_raw ctxt ts
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   515
  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   516
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   517
fun compile_validator_exprs_raw ctxt ts =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   518
  let val ts' = map (mk_validator_expr ctxt) ts in
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   519
    Code_Runtime.dynamic_value_strict
59154
68ca25931dce just one data slot per program unit;
wenzelm
parents: 59151
diff changeset
   520
      (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   521
      ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') []
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   522
  end
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42176
diff changeset
   523
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   524
fun compile_validator_exprs ctxt ts =
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   525
  compile_validator_exprs_raw ctxt ts
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   526
  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   527
46331
f5598b604a54 generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents: 46306
diff changeset
   528
fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T,  @{sort check_all})) Ts)
f5598b604a54 generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents: 46306
diff changeset
   529
f5598b604a54 generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents: 46306
diff changeset
   530
val test_goals =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   531
  Quickcheck_Common.generator_test_goal_terms
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   532
    ("exhaustive", (size_matters_for, compile_generator_expr))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   533
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   534
42308
e2abd1ca8d01 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
bulwahn
parents: 42307
diff changeset
   535
(* setup *)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   536
45484
23871e17dddb setting up exhaustive generators which are used for the smart generators
bulwahn
parents: 45420
diff changeset
   537
val setup_exhaustive_datatype_interpretation =
58659
6c9821c32dd5 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents: 58354
diff changeset
   538
  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive}
58186
a6c3962ea907 named interpretations
blanchet
parents: 58145
diff changeset
   539
    (@{sort exhaustive}, instantiate_exhaustive_datatype)
45484
23871e17dddb setting up exhaustive generators which are used for the smart generators
bulwahn
parents: 45420
diff changeset
   540
48178
0192811f0a96 exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents: 48013
diff changeset
   541
val setup_bounded_forall_datatype_interpretation =
58659
6c9821c32dd5 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents: 58354
diff changeset
   542
  BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs
58186
a6c3962ea907 named interpretations
blanchet
parents: 58145
diff changeset
   543
    (Quickcheck_Common.ensure_sort
a6c3962ea907 named interpretations
blanchet
parents: 58145
diff changeset
   544
       (((@{sort type}, @{sort type}), @{sort bounded_forall}),
58354
04ac60da613e support (finite values of) codatatypes in Quickcheck
blanchet
parents: 58225
diff changeset
   545
       (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
04ac60da613e support (finite values of) codatatypes in Quickcheck
blanchet
parents: 58225
diff changeset
   546
        instantiate_bounded_forall_datatype)))
48178
0192811f0a96 exporting important function for the "many conjecture refutation" compilation of quickcheck
bulwahn
parents: 48013
diff changeset
   547
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   548
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true)
43878
eeb10fdd9535 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents: 43877
diff changeset
   549
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   550
val _ =
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   551
  Theory.setup
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   552
   (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   553
      (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   554
    #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
2ed2eaabe3df modernized setup;
wenzelm
parents: 58659
diff changeset
   555
    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   556
    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)))
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   557
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61424
diff changeset
   558
end