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