author  haftmann 
Thu, 03 Jul 2008 11:16:08 +0200  
changeset 27454  fb6a272fe5d0 
parent 27103  d8549f4d900b 
child 28012  2308843f8b66 
permissions  rwrr 
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 

78 
text {* using builtin Haskell equality *} 

79 

80 
code_class eq 

81 
(Haskell "Eq" where "op =" \<equiv> "(==)") 

82 

83 
code_const "op =" 

84 
(Haskell infixl 4 "==") 

85 

86 

87 
text {* type bool *} 

88 

27454  89 
lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj 
24285  90 

91 
code_type bool 

92 
(SML "bool") 

93 
(OCaml "bool") 

94 
(Haskell "Bool") 

95 

96 
code_const True and False and Not and "op &" and "op " and If 

97 
(SML "true" and "false" and "not" 

98 
and infixl 1 "andalso" and infixl 0 "orelse" 

99 
and "!(if (_)/ then (_)/ else (_))") 

100 
(OCaml "true" and "false" and "not" 

101 
and infixl 4 "&&" and infixl 2 "" 

102 
and "!(if (_)/ then (_)/ else (_))") 

103 
(Haskell "True" and "False" and "not" 

104 
and infixl 3 "&&" and infixl 2 "" 

105 
and "!(if (_)/ then (_)/ else (_))") 

106 

107 
code_reserved SML 

108 
bool true false not 

109 

110 
code_reserved OCaml 

111 
bool not 

112 

113 

114 
text {* code generation for undefined as exception *} 

115 

116 
code_const undefined 

117 
(SML "raise/ Fail/ \"undefined\"") 

118 
(OCaml "failwith/ \"undefined\"") 

119 
(Haskell "error/ \"undefined\"") 

120 

121 

122 
text {* Let and If *} 

123 

124 
lemmas [code func] = Let_def if_True if_False 

125 

126 

127 
subsection {* Evaluation oracle *} 

128 

27103  129 
ML {* 
130 
structure Eval_Method = 

131 
struct 

132 

133 
val eval_ref : (unit > bool) option ref = ref NONE; 

134 

135 
end; 

136 
*} 

137 

24285  138 
oracle eval_oracle ("term") = {* fn thy => fn t => 
27103  139 
if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy 
140 
(HOLogic.dest_Trueprop t) [] 

24285  141 
then t 
142 
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) 

143 
*} 

144 

145 
method_setup eval = {* 

146 
let 

147 
fun eval_tac thy = 

148 
SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i) 

149 
in 

150 
Method.ctxt_args (fn ctxt => 

151 
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt))) 

152 
end 

153 
*} "solve goal by evaluation" 

154 

155 

156 
subsection {* Normalization by evaluation *} 

157 

158 
method_setup normalization = {* 

159 
Method.no_args (Method.SIMPLE_METHOD' 

25962  160 
(CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) 
161 
THEN' (fn k => TRY (rtac TrueI k)) 

25866  162 
)) 
24285  163 
*} "solve goal by normalization" 
164 

165 
end 