src/HOL/Library/Quickcheck.thy
author haftmann
Thu Feb 05 14:14:03 2009 +0100 (2009-02-05)
changeset 29808 b8b9d529663b
parent 29579 src/HOL/ex/Quickcheck.thy@cb520b766e00
child 29823 0ab754d13ccd
permissions -rw-r--r--
split of already properly working part of Quickcheck infrastructure
haftmann@29132
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@26265
     2
haftmann@26265
     3
header {* A simple counterexample generator *}
haftmann@26265
     4
haftmann@26265
     5
theory Quickcheck
haftmann@29132
     6
imports Random Code_Eval Map
haftmann@26265
     7
begin
haftmann@26265
     8
haftmann@26265
     9
subsection {* The @{text random} class *}
haftmann@26265
    10
haftmann@28335
    11
class random = typerep +
haftmann@26325
    12
  fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
haftmann@26265
    13
haftmann@26267
    14
text {* Type @{typ "'a itself"} *}
haftmann@26265
    15
haftmann@28335
    16
instantiation itself :: ("{type, typerep}") random
haftmann@26265
    17
begin
haftmann@26265
    18
haftmann@26265
    19
definition
haftmann@28335
    20
  "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
haftmann@26265
    21
haftmann@26265
    22
instance ..
haftmann@26265
    23
haftmann@26265
    24
end
haftmann@26265
    25
haftmann@26267
    26
haftmann@29808
    27
subsection {* Quickcheck generator *}
haftmann@29132
    28
haftmann@29132
    29
ML {*
haftmann@29132
    30
structure StateMonad =
haftmann@29132
    31
struct
haftmann@29132
    32
haftmann@29132
    33
fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
haftmann@29132
    34
fun liftT' sT = sT --> sT;
haftmann@29132
    35
haftmann@29808
    36
fun return T sT x = Const (@{const_name Pair}, T --> liftT T sT) $ x;
haftmann@29132
    37
haftmann@29132
    38
fun scomp T1 T2 sT f g = Const (@{const_name scomp},
haftmann@29132
    39
  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
haftmann@29132
    40
haftmann@29132
    41
end;
haftmann@29132
    42
haftmann@26265
    43
structure Quickcheck =
haftmann@26265
    44
struct
haftmann@26265
    45
haftmann@28309
    46
open Quickcheck;
haftmann@28309
    47
haftmann@26265
    48
val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
haftmann@26265
    49
haftmann@26325
    50
fun mk_generator_expr thy prop tys =
haftmann@26265
    51
  let
haftmann@26325
    52
    val bound_max = length tys - 1;
haftmann@26325
    53
    val bounds = map_index (fn (i, ty) =>
haftmann@26325
    54
      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
haftmann@26325
    55
    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
haftmann@26325
    56
    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
haftmann@26265
    57
    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
haftmann@26325
    58
      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
haftmann@26265
    59
    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
haftmann@26325
    60
    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
haftmann@26325
    61
    fun mk_split ty = Sign.mk_const thy
haftmann@26325
    62
      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
haftmann@26589
    63
    fun mk_scomp_split ty t t' =
haftmann@26589
    64
      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
haftmann@26325
    65
        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
haftmann@26589
    66
    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
haftmann@26325
    67
      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
haftmann@26265
    68
    val t = fold_rev mk_bindclause bounds (return $ check);
haftmann@26265
    69
  in Abs ("n", @{typ index}, t) end;
haftmann@26265
    70
haftmann@28309
    71
fun compile_generator_expr thy t =
haftmann@26265
    72
  let
haftmann@28309
    73
    val tys = (map snd o fst o strip_abs) t;
haftmann@28309
    74
    val t' = mk_generator_expr thy t tys;
haftmann@28309
    75
    val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' [];
haftmann@28309
    76
  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
haftmann@26265
    77
haftmann@26265
    78
end
haftmann@26265
    79
*}
haftmann@26265
    80
haftmann@28309
    81
setup {*
haftmann@28309
    82
  Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
haftmann@28309
    83
*}
haftmann@28309
    84
haftmann@26265
    85
end