author | haftmann |
Thu, 28 Aug 2008 22:09:20 +0200 | |
changeset 28054 | 2b84d34c5d02 |
parent 28012 | 2308843f8b66 |
child 28290 | 4cc2b6046258 |
permissions | -rw-r--r-- |
24285 | 1 |
(* Title: HOL/Code_Setup.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann |
|
4 |
*) |
|
5 |
||
6 |
header {* Setup of code generators and derived tools *} |
|
7 |
||
8 |
theory Code_Setup |
|
9 |
imports HOL |
|
10 |
uses "~~/src/HOL/Tools/recfun_codegen.ML" |
|
11 |
begin |
|
12 |
||
13 |
subsection {* SML code generator setup *} |
|
14 |
||
15 |
setup RecfunCodegen.setup |
|
16 |
||
17 |
types_code |
|
18 |
"bool" ("bool") |
|
19 |
attach (term_of) {* |
|
20 |
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
|
21 |
*} |
|
22 |
attach (test) {* |
|
25885 | 23 |
fun gen_bool i = |
24 |
let val b = one_of [false, true] |
|
25 |
in (b, fn () => term_of_bool b) end; |
|
24285 | 26 |
*} |
27 |
"prop" ("bool") |
|
28 |
attach (term_of) {* |
|
29 |
fun term_of_prop b = |
|
30 |
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); |
|
31 |
*} |
|
32 |
||
33 |
consts_code |
|
34 |
"Trueprop" ("(_)") |
|
35 |
"True" ("true") |
|
36 |
"False" ("false") |
|
37 |
"Not" ("Bool.not") |
|
38 |
"op |" ("(_ orelse/ _)") |
|
39 |
"op &" ("(_ andalso/ _)") |
|
40 |
"If" ("(if _/ then _/ else _)") |
|
41 |
||
42 |
setup {* |
|
43 |
let |
|
44 |
||
45 |
fun eq_codegen thy defs gr dep thyname b t = |
|
46 |
(case strip_comb t of |
|
47 |
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
|
48 |
| (Const ("op =", _), [t, u]) => |
|
49 |
let |
|
50 |
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); |
|
51 |
val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); |
|
52 |
val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) |
|
53 |
in |
|
54 |
SOME (gr''', Codegen.parens |
|
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
25962
diff
changeset
|
55 |
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu])) |
24285 | 56 |
end |
57 |
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
|
58 |
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) |
|
59 |
| _ => NONE); |
|
60 |
||
61 |
in |
|
62 |
Codegen.add_codegen "eq_codegen" eq_codegen |
|
63 |
end |
|
64 |
*} |
|
65 |
||
24463
841c2e24761f
Smaller size and fewer iterations for quickcheck.
berghofe
parents:
24293
diff
changeset
|
66 |
quickcheck_params [size = 5, iterations = 50] |
841c2e24761f
Smaller size and fewer iterations for quickcheck.
berghofe
parents:
24293
diff
changeset
|
67 |
|
24285 | 68 |
text {* Evaluation *} |
69 |
||
70 |
method_setup evaluation = {* |
|
71 |
Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI)) |
|
72 |
*} "solve goal by evaluation" |
|
73 |
||
74 |
||
75 |
subsection {* Generic code generator setup *} |
|
76 |
||
77 |
text {* using built-in Haskell equality *} |
|
78 |
||
79 |
code_class eq |
|
80 |
(Haskell "Eq" where "op =" \<equiv> "(==)") |
|
81 |
||
82 |
code_const "op =" |
|
83 |
(Haskell infixl 4 "==") |
|
84 |
||
85 |
||
86 |
text {* type bool *} |
|
87 |
||
88 |
code_type bool |
|
89 |
(SML "bool") |
|
90 |
(OCaml "bool") |
|
91 |
(Haskell "Bool") |
|
92 |
||
93 |
code_const True and False and Not and "op &" and "op |" and If |
|
94 |
(SML "true" and "false" and "not" |
|
95 |
and infixl 1 "andalso" and infixl 0 "orelse" |
|
96 |
and "!(if (_)/ then (_)/ else (_))") |
|
97 |
(OCaml "true" and "false" and "not" |
|
98 |
and infixl 4 "&&" and infixl 2 "||" |
|
99 |
and "!(if (_)/ then (_)/ else (_))") |
|
100 |
(Haskell "True" and "False" and "not" |
|
101 |
and infixl 3 "&&" and infixl 2 "||" |
|
102 |
and "!(if (_)/ then (_)/ else (_))") |
|
103 |
||
104 |
code_reserved SML |
|
105 |
bool true false not |
|
106 |
||
107 |
code_reserved OCaml |
|
108 |
bool not |
|
109 |
||
110 |
||
111 |
text {* code generation for undefined as exception *} |
|
112 |
||
28012 | 113 |
code_abort undefined |
114 |
||
24285 | 115 |
code_const undefined |
116 |
(SML "raise/ Fail/ \"undefined\"") |
|
117 |
(OCaml "failwith/ \"undefined\"") |
|
118 |
(Haskell "error/ \"undefined\"") |
|
119 |
||
120 |
||
121 |
subsection {* Evaluation oracle *} |
|
122 |
||
27103 | 123 |
ML {* |
124 |
structure Eval_Method = |
|
125 |
struct |
|
126 |
||
127 |
val eval_ref : (unit -> bool) option ref = ref NONE; |
|
128 |
||
129 |
end; |
|
130 |
*} |
|
131 |
||
24285 | 132 |
oracle eval_oracle ("term") = {* fn thy => fn t => |
28054 | 133 |
if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy |
27103 | 134 |
(HOLogic.dest_Trueprop t) [] |
24285 | 135 |
then t |
136 |
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) |
|
137 |
*} |
|
138 |
||
139 |
method_setup eval = {* |
|
140 |
let |
|
141 |
fun eval_tac thy = |
|
142 |
SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i) |
|
143 |
in |
|
144 |
Method.ctxt_args (fn ctxt => |
|
145 |
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt))) |
|
146 |
end |
|
147 |
*} "solve goal by evaluation" |
|
148 |
||
149 |
||
150 |
subsection {* Normalization by evaluation *} |
|
151 |
||
152 |
method_setup normalization = {* |
|
153 |
Method.no_args (Method.SIMPLE_METHOD' |
|
25962 | 154 |
(CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) |
155 |
THEN' (fn k => TRY (rtac TrueI k)) |
|
25866 | 156 |
)) |
24285 | 157 |
*} "solve goal by normalization" |
158 |
||
159 |
end |