src/HOL/Tools/Quickcheck/quickcheck_common.ML
author bulwahn
Mon, 23 Jan 2012 14:06:19 +0100
changeset 46312 518cc38a1a8c
parent 45923 473b744c23f2
child 46327 ecda23528833
permissions -rw-r--r--
adding fun_eq_iff to the preprocessing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     1
(*  Title:      HOL/Tools/Quickcheck/quickcheck_common.ML
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     2
    Author:     Florian Haftmann, Lukas Bulwahn, TU Muenchen
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     3
41938
645cca858c69 tuned headers;
wenzelm
parents: 41935
diff changeset
     4
Common functions for quickcheck's generators.
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     5
*)
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     6
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     7
signature QUICKCHECK_COMMON =
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
     8
sig
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
     9
  val strip_imp : term -> (term list * term)
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45719
diff changeset
    10
  val reflect_bool : bool -> term
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    11
  val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    12
    -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    13
  val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    14
    -> (string * sort -> string * sort) option
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    15
  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    16
    -> (typ option * (term * term list)) list list
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
    17
  val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    18
  val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    19
  type compile_generator =
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    20
    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
    21
  val generator_test_goal_terms :
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
    22
    string * compile_generator -> Proof.context -> bool -> (string * typ) list
45418
e5ef7aa77fde removing extra arguments
bulwahn
parents: 45417
diff changeset
    23
    -> (term * term list) list -> Quickcheck.result list
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    24
  type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    25
     -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    26
  val ensure_sort :
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    27
    (((sort * sort) * sort) *
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    28
      ((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    29
        * string * (string list * string list) * (typ list * typ list)) * instantiation))
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    30
    -> Datatype.config -> string list -> theory -> theory
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    31
  val ensure_common_sort_datatype :
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    32
    (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
    33
  val datatype_interpretation : (sort * instantiation) -> theory -> theory
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
    34
  val gen_mk_parametric_generator_expr :
42229
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
    35
   (((Proof.context -> term * term list -> term) * term) * typ)
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
    36
     -> Proof.context -> (term * term list) list -> term
45039
632a033616e9 adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents: 44241
diff changeset
    37
  val mk_fun_upd : typ -> typ -> term * term -> term -> term
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
    38
  val post_process_term : term -> term
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
    39
  val test_term : string * compile_generator
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
    40
    -> Proof.context -> bool -> term * term list -> Quickcheck.result
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    41
end;
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    42
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    43
structure Quickcheck_Common : QUICKCHECK_COMMON =
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    44
struct
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
    45
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    46
(* static options *)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    47
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    48
val define_foundationally = false
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    49
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
    50
(* HOLogic's term functions *)
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
    51
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
    52
fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
    53
  | strip_imp A = ([], A)
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42159
diff changeset
    54
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45719
diff changeset
    55
fun reflect_bool b = if b then @{term "True"} else @{term "False"}
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45719
diff changeset
    56
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
    57
fun mk_undefined T = Const(@{const_name undefined}, T)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    58
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    59
(* testing functions: testing with increasing sizes (and cardinalities) *)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    60
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    61
type compile_generator =
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    62
  Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    63
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    64
fun check_test_term t =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    65
  let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    66
    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    67
      error "Term to be tested contains type variables";
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    68
    val _ = null (Term.add_vars t []) orelse
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    69
      error "Term to be tested contains schematic variables";
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    70
  in () end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    71
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    72
fun cpu_time description e =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    73
  let val ({cpu, ...}, result) = Timing.timing e ()
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    74
  in (result, (description, Time.toMilliseconds cpu)) end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    75
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
    76
fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    77
  let
45757
e32dd098f57a renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents: 45755
diff changeset
    78
    val genuine_only = Config.get ctxt Quickcheck.genuine_only
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    79
    val _ = check_test_term t
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    80
    val names = Term.add_free_names t []
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    81
    val current_size = Unsynchronized.ref 0
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    82
    val current_result = Unsynchronized.ref Quickcheck.empty_result 
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    83
    fun excipit () =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    84
      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    85
    val act = if catch_code_errors then try else (fn f => SOME o f) 
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    86
    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    87
        (fn () => act (compile ctxt) [(t, eval_terms)]);
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    88
    val _ = Quickcheck.add_timing comp_time current_result
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    89
    fun with_size test_fun genuine_only k =
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    90
      if k > Config.get ctxt Quickcheck.size then
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    91
        NONE
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    92
      else
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    93
        let
45765
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
    94
          val _ = Quickcheck.verbose_message ctxt
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    95
            ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    96
          val _ = current_size := k
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    97
          val ((result, report), timing) =
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
    98
            cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
    99
          val _ = Quickcheck.add_timing timing current_result
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   100
          val _ = Quickcheck.add_report k report current_result
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   101
        in
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   102
          case result of
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   103
            NONE => with_size test_fun genuine_only (k + 1)
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   104
          | SOME (true, ts) => SOME (true, ts)
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   105
          | SOME (false, ts) =>
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   106
            let
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   107
              val (ts1, ts2) = chop (length names) ts
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   108
              val (eval_terms', _) = chop (length ts2) eval_terms
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   109
              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   110
            in
45765
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
   111
              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
   112
              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   113
              with_size test_fun true k)
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   114
            end
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   115
        end;
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   116
  in
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   117
    case test_fun of
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   118
      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   119
        !current_result)
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   120
    | SOME test_fun =>
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   121
      let
45819
b85bb803bcf3 tuned quickcheck's response
bulwahn
parents: 45792
diff changeset
   122
        val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   123
        val (response, exec_time) =
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   124
          cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   125
        val _ = Quickcheck.add_response names eval_terms response current_result
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   126
        val _ = Quickcheck.add_timing exec_time current_result
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   127
      in !current_result end
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   128
  end;
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   129
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   130
fun validate_terms ctxt ts =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   131
  let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   132
    val _ = map check_test_term ts
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   133
    val size = Config.get ctxt Quickcheck.size
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   134
    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   135
      (fn () => Quickcheck.mk_batch_validator ctxt ts) 
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   136
    fun with_size tester k =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   137
      if k > size then true
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   138
      else if tester k then with_size tester (k + 1) else false
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   139
    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   140
        Option.map (map (fn test_fun =>
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   141
          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   142
              (fn () => with_size test_fun 1) ()
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   143
             handle TimeLimit.TimeOut => true)) test_funs)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   144
  in
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   145
    (results, [comp_time, exec_time])
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   146
  end
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   147
  
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   148
fun test_terms ctxt ts =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   149
  let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   150
    val _ = map check_test_term ts
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   151
    val size = Config.get ctxt Quickcheck.size
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   152
    val namess = map (fn t => Term.add_free_names t []) ts
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   153
    val (test_funs, comp_time) =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   154
      cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   155
    fun with_size tester k =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   156
      if k > size then NONE
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   157
      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   158
    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   159
        Option.map (map (fn test_fun =>
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   160
          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   161
              (fn () => with_size test_fun 1) ()
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   162
             handle TimeLimit.TimeOut => NONE)) test_funs)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   163
  in
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   164
    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   165
      [comp_time, exec_time])
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   166
  end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   167
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   168
fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   169
  let
45757
e32dd098f57a renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents: 45755
diff changeset
   170
    val genuine_only = Config.get ctxt Quickcheck.genuine_only
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   171
    val thy = Proof_Context.theory_of ctxt
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   172
    val (ts', eval_terms) = split_list ts
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   173
    val _ = map check_test_term ts'
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   174
    val names = Term.add_free_names (hd ts') []
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   175
    val Ts = map snd (Term.add_frees (hd ts') [])
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   176
    val current_result = Unsynchronized.ref Quickcheck.empty_result
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   177
    fun test_card_size test_fun genuine_only (card, size) =
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   178
      (* FIXME: why decrement size by one? *)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   179
      let
45686
cf22004ad55d adding more verbose messages to exhaustive quickcheck
bulwahn
parents: 45639
diff changeset
   180
        val _ =
45765
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
   181
          Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
45686
cf22004ad55d adding more verbose messages to exhaustive quickcheck
bulwahn
parents: 45639
diff changeset
   182
            (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
cf22004ad55d adding more verbose messages to exhaustive quickcheck
bulwahn
parents: 45639
diff changeset
   183
            "cardinality: " ^ string_of_int card)          
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   184
        val (ts, timing) =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   185
          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   186
            (fn () => fst (test_fun genuine_only [card, size - 1]))
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   187
        val _ = Quickcheck.add_timing timing current_result
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   188
      in
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   189
        Option.map (pair (card, size)) ts
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   190
      end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   191
    val enumeration_card_size =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   192
      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   193
        (* size does not matter *)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   194
        map (rpair 0) (1 upto (length ts))
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   195
      else
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   196
        (* size does matter *)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   197
        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   198
        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
45419
10ba32c347b0 quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents: 45418
diff changeset
   199
    val act = if catch_code_errors then try else (fn f => SOME o f)
10ba32c347b0 quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents: 45418
diff changeset
   200
    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts)
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   201
    val _ = Quickcheck.add_timing comp_time current_result
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   202
  in
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   203
    case test_fun of
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   204
      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   205
        !current_result)
45417
cae3ba9be892 removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents: 45416
diff changeset
   206
    | SOME test_fun =>
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   207
      let
45921
bulwahn
parents: 45819
diff changeset
   208
        val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   209
        fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   210
          SOME ((card, _), (true, ts)) =>
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   211
            Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   212
        | SOME ((card, size), (false, ts)) =>
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   213
           let
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   214
              val (ts1, ts2) = chop (length names) ts
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   215
              val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   216
              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   217
            in
45765
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
   218
              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
cb6ddee6a463 making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents: 45763
diff changeset
   219
              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   220
              test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   221
            end
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   222
        | NONE => ()
45755
b27a06dfb2ef outputing the potentially spurious counterexample and continue search
bulwahn
parents: 45754
diff changeset
   223
      in (test genuine_only enumeration_card_size; !current_result) end
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   224
  end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   225
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   226
fun get_finite_types ctxt =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   227
  fst (chop (Config.get ctxt Quickcheck.finite_type_size)
45416
bulwahn
parents: 45159
diff changeset
   228
    [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"},
bulwahn
parents: 45159
diff changeset
   229
     @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}])
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   230
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   231
exception WELLSORTED of string
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   232
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   233
fun monomorphic_term thy insts default_T =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   234
  let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   235
    fun subst (T as TFree (v, S)) =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   236
      let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   237
        val T' = AList.lookup (op =) insts v
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   238
          |> the_default default_T
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   239
      in if Sign.of_sort thy (T', S) then T'
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   240
        else raise (WELLSORTED ("For instantiation with default_type " ^
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   241
          Syntax.string_of_typ_global thy default_T ^
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   242
          ":\n" ^ Syntax.string_of_typ_global thy T' ^
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   243
          " to be substituted for variable " ^
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   244
          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   245
          Syntax.string_of_sort_global thy S))
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   246
      end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   247
      | subst T = T;
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   248
  in (map_types o map_atyps) subst end;
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   249
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   250
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   251
45440
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   252
(* minimalistic preprocessing *)
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   253
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   254
fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = 
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   255
  let
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   256
    val (a', t') = strip_all t
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   257
  in ((a, T) :: a', t') end
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   258
  | strip_all t = ([], t);
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   259
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   260
fun preprocess ctxt t =
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   261
  let
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   262
    val thy = Proof_Context.theory_of ctxt
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   263
    val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   264
    val rewrs = map (swap o dest) @{thms all_simps} @
46312
518cc38a1a8c adding fun_eq_iff to the preprocessing
bulwahn
parents: 45923
diff changeset
   265
      (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}])
45440
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   266
    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   267
    val (vs, body) = strip_all t'
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   268
    val vs' = Variable.variant_frees ctxt [t'] vs
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   269
  in
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   270
    subst_bounds (map Free (rev vs'), body)
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   271
  end
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   272
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   273
(* instantiation of type variables with concrete types *)
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   274
 
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   275
fun instantiate_goals lthy insts goals =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   276
  let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   277
    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   278
    val thy = Proof_Context.theory_of lthy
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   279
    val default_insts =
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   280
      if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   281
    val inst_goals =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   282
      map (fn (check_goal, eval_terms) =>
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   283
        if not (null (Term.add_tfree_names check_goal [])) then
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   284
          map (fn T =>
45440
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   285
            (pair (SOME T) o Term o apfst (preprocess lthy))
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   286
              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   287
              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   288
        else
45440
9f4d3e68ae98 adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents: 45420
diff changeset
   289
          [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   290
    val error_msg =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   291
      cat_lines
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   292
        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   293
    fun is_wellsorted_term (T, Term t) = SOME (T, t)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   294
      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   295
    val correct_inst_goals =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   296
      case map (map_filter is_wellsorted_term) inst_goals of
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   297
        [[]] => error error_msg
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   298
      | xs => xs
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   299
    val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   300
  in
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   301
    correct_inst_goals
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   302
  end
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   303
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45687
diff changeset
   304
(* compilation of testing functions *)
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45687
diff changeset
   305
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
   306
fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   307
  let
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
   308
    val T = fastype_of then_t
45754
394ecd91434a dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents: 45753
diff changeset
   309
    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   310
  in
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   311
    Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $ 
45761
90028fd2f1fa exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents: 45757
diff changeset
   312
      (if_t $ cond $ then_t $ else_t genuine) $
45763
3bb2bdf654f7 random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents: 45761
diff changeset
   313
      (if_t $ genuine_only $ none $ else_t false)
45753
196697f71488 indicating where the restart should occur; making safe_if dynamic
bulwahn
parents: 45728
diff changeset
   314
  end
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45687
diff changeset
   315
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   316
fun collect_results f [] results = results
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   317
  | collect_results f (t :: ts) results =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   318
    let
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   319
      val result = f t
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   320
    in
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   321
      if Quickcheck.found_counterexample result then
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   322
        (result :: results)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   323
      else
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   324
        collect_results f ts (result :: results)
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   325
    end  
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   326
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   327
fun generator_test_goal_terms (name, compile) ctxt catch_code_errors insts goals =
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   328
  let
45687
a07654c67f30 quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents: 45686
diff changeset
   329
    fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
a07654c67f30 quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents: 45686
diff changeset
   330
    fun add_equation_eval_terms (t, eval_terms) =
a07654c67f30 quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents: 45686
diff changeset
   331
      case try HOLogic.dest_eq (snd (strip_imp t)) of
a07654c67f30 quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents: 45686
diff changeset
   332
        SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms))
a07654c67f30 quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents: 45686
diff changeset
   333
      | NONE => (t, eval_terms)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   334
    fun test_term' goal =
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   335
      case goal of
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   336
        [(NONE, t)] => test_term (name, compile) ctxt catch_code_errors t
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   337
      | ts => test_term_with_cardinality (name, compile) ctxt catch_code_errors (map snd ts)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   338
    val goals' = instantiate_goals ctxt insts goals
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   339
      |> map (map (apsnd add_equation_eval_terms))
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   340
  in
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   341
    if Config.get ctxt Quickcheck.finite_types then
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   342
      collect_results test_term' goals' []
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   343
    else
45420
d17556b9a89b more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents: 45419
diff changeset
   344
      collect_results (test_term (name, compile) ctxt catch_code_errors)
45159
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   345
        (maps (map snd) goals') []
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   346
  end;
3f1d1ce024cb moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents: 45039
diff changeset
   347
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   348
(* defining functions *)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   349
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   350
fun pat_completeness_auto ctxt =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   351
  Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   352
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   353
fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   354
  if define_foundationally andalso is_some termination_tac then
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   355
    let
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   356
      val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   357
    in
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   358
      Function.add_function
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 42229
diff changeset
   359
        (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 42229
diff changeset
   360
          (names ~~ Ts))
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 42229
diff changeset
   361
        (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   362
        Function_Common.default_config pat_completeness_auto
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   363
      #> snd
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   364
      #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   365
      #> snd
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   366
    end
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   367
  else
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   368
    fold_map (fn (name, T) => Local_Theory.define
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   369
        ((Binding.conceal (Binding.name name), NoSyn),
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   370
          (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   371
      #> apfst fst) (names ~~ Ts)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   372
    #> (fn (consts, lthy) =>
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   373
      let
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   374
        val eqs_t = mk_equations consts
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   375
        val eqs = map (fn eq => Goal.prove lthy argnames [] eq
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42287
diff changeset
   376
          (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   377
      in
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   378
        fold (fn (name, eq) => Local_Theory.note
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45440
diff changeset
   379
          ((Binding.conceal
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45440
diff changeset
   380
            (Binding.qualify true prfx
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45440
diff changeset
   381
              (Binding.qualify true name (Binding.name "simps"))),
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45440
diff changeset
   382
             Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), [eq]) #> snd)
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45440
diff changeset
   383
          (names ~~ eqs) lthy
42214
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   384
      end)
9ca13615c619 refactoring generator definition in quickcheck and removing clone
bulwahn
parents: 42195
diff changeset
   385
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   386
(** ensuring sort constraints **)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   387
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   388
type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   389
  -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   390
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   391
fun perhaps_constrain thy insts raw_vs =
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   392
  let
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   393
    fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   394
      (Logic.varifyT_global T, sort);
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   395
    val vtab = Vartab.empty
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   396
      |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   397
      |> fold meet insts;
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   398
  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   399
  end handle Sorts.CLASS_ERROR _ => NONE;
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   400
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   401
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   402
  let
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   403
    val algebra = Sign.classes_of thy;
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   404
    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
42229
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   405
    val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   406
    fun insts_of sort constr  = (map (rpair sort) o flat o maps snd o maps snd)
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   407
      (Datatype_Aux.interpret_construction descr vs constr)
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   408
    val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   409
      @ insts_of aux_sort { atyp = K [], dtyp = K o K }
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   410
    val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   411
  in if has_inst then thy
42229
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   412
    else case perhaps_constrain thy insts vs
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   413
     of SOME constrain => instantiate config descr
42229
1491b7209e76 generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents: 42214
diff changeset
   414
          (map constrain vs) tycos prfx (names, auxnames)
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   415
            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   416
      | NONE => thy
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   417
  end;
45923
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   418
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   419
fun ensure_common_sort_datatype (sort, instantiate) =
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   420
  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   421
473b744c23f2 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents: 45921
diff changeset
   422
val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   423
  
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   424
(** generic parametric compilation **)
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   425
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   426
fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   427
  let
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   428
    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
45721
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45719
diff changeset
   429
    fun mk_if (index, (t, eval_terms)) else_t = if_t $
d1fb55c2ed65 quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents: 45719
diff changeset
   430
        (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   431
        (mk_generator_expr ctxt (t, eval_terms)) $ else_t
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   432
  in
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42793
diff changeset
   433
    absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
42159
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   434
  end
234ec7011e5d generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents: 42110
diff changeset
   435
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   436
(** post-processing of function terms **)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   437
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   438
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   439
  | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   440
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   441
fun mk_fun_upd T1 T2 (t1, t2) t = 
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   442
  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   443
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   444
fun dest_fun_upds t =
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   445
  case try dest_fun_upd t of
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   446
    NONE =>
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   447
      (case t of
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   448
        Abs (_, _, _) => ([], t) 
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   449
      | _ => raise TERM ("dest_fun_upds", [t]))
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   450
  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   451
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   452
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   453
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   454
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   455
  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   456
  | make_set T1 ((t1, @{const True}) :: tps) =
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   457
    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   458
      $ t1 $ (make_set T1 tps)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   459
  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   460
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   461
fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   462
  | make_coset T tps = 
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   463
    let
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   464
      val U = T --> @{typ bool}
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   465
      fun invert @{const False} = @{const True}
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   466
        | invert @{const True} = @{const False}
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   467
    in
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   468
      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   469
        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   470
    end
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   471
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   472
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   473
  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   474
  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   475
  
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   476
fun post_process_term t =
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   477
  let
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   478
    fun map_Abs f t =
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   479
      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   480
    fun process_args t = case strip_comb t of
42110
17e0cd9bc259 fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents: 41938
diff changeset
   481
      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   482
  in
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   483
    case fastype_of t of
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   484
      Type (@{type_name fun}, [T1, T2]) =>
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   485
        (case try dest_fun_upds t of
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   486
          SOME (tps, t) =>
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   487
            (map (pairself post_process_term) tps, map_Abs post_process_term t)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   488
            |> (case T2 of
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   489
              @{typ bool} => 
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   490
                (case t of
42110
17e0cd9bc259 fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents: 41938
diff changeset
   491
                   Abs(_, _, @{const False}) => fst #> rev #> make_set T1
17e0cd9bc259 fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents: 41938
diff changeset
   492
                 | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   493
                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   494
                 | _ => raise TERM ("post_process_term", [t]))
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   495
            | Type (@{type_name option}, _) =>
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   496
                (case t of
42110
17e0cd9bc259 fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents: 41938
diff changeset
   497
                  Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   498
                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
42110
17e0cd9bc259 fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents: 41938
diff changeset
   499
                | _ => make_fun_upds T1 T2)
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   500
            | _ => make_fun_upds T1 T2)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   501
        | NONE => process_args t)
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   502
    | _ => process_args t
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41927
diff changeset
   503
  end
41927
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   504
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff changeset
   505
end;