47 (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); |
47 (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); |
48 fun mk_scomp_split ty t t' = |
48 fun mk_scomp_split ty t t' = |
49 mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t |
49 mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t |
50 (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t'))); |
50 (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t'))); |
51 fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty |
51 fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty |
52 (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i); |
52 (Sign.mk_const thy (@{const_name Quickcheck.random}, [ty]) $ Bound i); |
53 in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; |
53 in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; |
54 |
54 |
55 fun compile_generator_expr thy t = |
55 fun compile_generator_expr thy t = |
56 let |
56 let |
57 val tys = (map snd o fst o strip_abs) t; |
57 val tys = (map snd o fst o strip_abs) t; |
96 val T = Type (tyco, Ts); |
96 val T = Type (tyco, Ts); |
97 fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) |
97 fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) |
98 val Ttm = mk_termifyT T; |
98 val Ttm = mk_termifyT T; |
99 val typtm = mk_termifyT typ; |
99 val typtm = mk_termifyT typ; |
100 fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); |
100 fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); |
101 fun mk_random T = mk_const @{const_name random} [T]; |
101 fun mk_random T = mk_const @{const_name Quickcheck.random} [T]; |
102 val size = @{term "j::code_numeral"}; |
102 val size = @{term "j::code_numeral"}; |
103 val v = "x"; |
103 val v = "x"; |
104 val t_v = Free (v, typtm); |
104 val t_v = Free (v, typtm); |
105 val t_constr = mk_const constr Ts; |
105 val t_constr = mk_const constr Ts; |
106 val lhs = mk_random T $ size; |
106 val lhs = mk_random T $ size; |