equal
deleted
inserted
replaced
15 subsection {* Configuration of the code generator *} |
15 subsection {* Configuration of the code generator *} |
16 |
16 |
17 types_code |
17 types_code |
18 "bool" ("bool") |
18 "bool" ("bool") |
19 "*" ("(_ */ _)") |
19 "*" ("(_ */ _)") |
20 "list" ("_ list") |
|
21 |
20 |
22 consts_code |
21 consts_code |
23 "True" ("true") |
22 "True" ("true") |
24 "False" ("false") |
23 "False" ("false") |
25 "Not" ("not") |
24 "Not" ("not") |
29 |
28 |
30 "Pair" ("(_,/ _)") |
29 "Pair" ("(_,/ _)") |
31 "fst" ("fst") |
30 "fst" ("fst") |
32 "snd" ("snd") |
31 "snd" ("snd") |
33 |
32 |
34 "Nil" ("[]") |
|
35 "Cons" ("(_ ::/ _)") |
|
36 |
|
37 "wfrec" ("wf'_rec?") |
33 "wfrec" ("wf'_rec?") |
38 |
34 |
39 quickcheck_params [default_type = int] |
35 quickcheck_params [default_type = int] |
40 |
36 |
41 ML {* |
37 ML {* |
42 fun wf_rec f x = f (wf_rec f) x; |
38 fun wf_rec f x = f (wf_rec f) x; |
43 |
39 |
44 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
40 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
45 val term_of_list = HOLogic.mk_list; |
|
46 val term_of_int = HOLogic.mk_int; |
41 val term_of_int = HOLogic.mk_int; |
47 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y; |
42 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y; |
48 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U); |
43 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U); |
49 |
44 |
50 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" |
45 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" |
62 | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen |
57 | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen |
63 thy dep b (gr, Codegen.eta_expand t ts 2)) |
58 thy dep b (gr, Codegen.eta_expand t ts 2)) |
64 | _ => None))]; |
59 | _ => None))]; |
65 |
60 |
66 fun gen_bool i = one_of [false, true]; |
61 fun gen_bool i = one_of [false, true]; |
67 |
|
68 fun gen_list' aG i j = frequency |
|
69 [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] () |
|
70 and gen_list aG i = gen_list' aG i i; |
|
71 |
62 |
72 fun gen_int i = one_of [~1, 1] * random_range 0 i; |
63 fun gen_int i = one_of [~1, 1] * random_range 0 i; |
73 |
64 |
74 fun gen_id_42 aG bG i = (aG i, bG i); |
65 fun gen_id_42 aG bG i = (aG i, bG i); |
75 |
66 |