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