author  haftmann 
Thu, 23 Feb 2012 21:25:59 +0100  
changeset 46635  cde737f9c911 
parent 42979  5b9e16259341 
child 46638  fc315796794e 
permissions  rwrr 
32657  1 
(* Title: HOL/Code_Evaluation.thy 
28228  2 
Author: Florian Haftmann, TU Muenchen 
3 
*) 

4 

5 
header {* Term evaluation using the generic code generator *} 

6 

32657  7 
theory Code_Evaluation 
46635
cde737f9c911
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
42979
diff
changeset

8 
imports Plain Typerep Code_Numeral Predicate 
39564  9 
uses ("Tools/code_evaluation.ML") 
28228  10 
begin 
11 

12 
subsection {* Term representation *} 

13 

14 
subsubsection {* Terms and class @{text term_of} *} 

15 

16 
datatype "term" = dummy_term 

17 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

18 
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 
28228  19 
"Const _ _ = dummy_term" 
20 

28661  21 
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where 
28228  22 
"App _ _ = dummy_term" 
23 

40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

24 
definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where 
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

25 
"Abs _ _ _ = dummy_term" 
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

26 

42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

27 
definition Free :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

28 
"Free _ _ = dummy_term" 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

29 

5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

30 
code_datatype Const App Abs Free 
28228  31 

28335  32 
class term_of = typerep + 
31031  33 
fixes term_of :: "'a \<Rightarrow> term" 
28228  34 

35 
lemma term_of_anything: "term_of x \<equiv> t" 

36 
by (rule eq_reflection) (cases "term_of x", cases t, simp) 

37 

31191  38 
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) 
31178  39 
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where 
31191  40 
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" 
31178  41 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

42 
lemma valapp_code [code, code_unfold]: 
31191  43 
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" 
44 
by (simp only: valapp_def fst_conv snd_conv) 

31178  45 

28228  46 

31178  47 
subsubsection {* Syntax *} 
48 

31191  49 
definition termify :: "'a \<Rightarrow> term" where 
50 
[code del]: "termify x = dummy_term" 

51 

52 
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where 

53 
"valtermify x \<equiv> (x, \<lambda>u. termify x)" 

31178  54 

55 
locale term_syntax 

56 
begin 

57 

31191  58 
notation App (infixl "<\<cdot>>" 70) 
59 
and valapp (infixl "{\<cdot>}" 70) 

31178  60 

61 
end 

62 

63 
interpretation term_syntax . 

64 

31191  65 
no_notation App (infixl "<\<cdot>>" 70) 
66 
and valapp (infixl "{\<cdot>}" 70) 

67 

68 

39564  69 
subsection {* Tools setup and evaluation *} 
70 

39567
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

71 
lemma eq_eq_TrueD: 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

72 
assumes "(x \<equiv> y) \<equiv> Trueprop True" 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

73 
shows "x \<equiv> y" 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

74 
using assms by simp 
5ee997fbe5cc
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
haftmann
parents:
39564
diff
changeset

75 

39564  76 
use "Tools/code_evaluation.ML" 
77 

78 
code_reserved Eval Code_Evaluation 

79 

80 
setup {* Code_Evaluation.setup *} 

81 

82 

83 
subsection {* @{text term_of} instances *} 

84 

85 
instantiation "fun" :: (typerep, typerep) term_of 

86 
begin 

87 

88 
definition 

89 
"term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') 

90 
[Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" 

91 

92 
instance .. 

93 

94 
end 

95 

96 
instantiation String.literal :: term_of 

97 
begin 

98 

99 
definition 

100 
"term_of s = App (Const (STR ''STR'') 

101 
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], 

102 
Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" 

103 

104 
instance .. 

105 

106 
end 

107 

108 

109 
subsubsection {* Code generator setup *} 

110 

111 
lemmas [code del] = term.recs term.cases term.size 

112 
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" .. 

113 

114 
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. 

115 
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. 

116 
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" .. 

117 
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) 

118 
= Code_Evaluation.term_of" .. 

119 
lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) 

120 
= Code_Evaluation.term_of" .. 

121 

122 
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: 

123 
"Code_Evaluation.term_of c = 

124 
(let (n, m) = nibble_pair_of_char c 

125 
in Code_Evaluation.App (Code_Evaluation.App 

126 
(Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) 

127 
(Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" 

128 
by (subst term_of_anything) rule 

129 

130 
code_type "term" 

131 
(Eval "Term.term") 

132 

42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

133 
code_const Const and App and Abs and Free 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

134 
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))" 
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

135 
and "Term.Free/ ((_), (_))") 
39564  136 

137 
code_const "term_of \<Colon> String.literal \<Rightarrow> term" 

138 
(Eval "HOLogic.mk'_literal") 

139 

140 
code_reserved Eval HOLogic 

141 

142 

143 
subsubsection {* Numeric types *} 

31191  144 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

145 
definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

146 
"term_of_num_semiring two = (\<lambda>_. dummy_term)" 
31191  147 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

148 
lemma (in term_syntax) term_of_num_semiring_code [code]: 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

149 
"term_of_num_semiring two k = (if k = 0 then termify Int.Pls 
31191  150 
else (if k mod two = 0 
40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

151 
then termify Int.Bit0 <\<cdot>> term_of_num_semiring two (k div two) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

152 
else termify Int.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))" 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

153 
by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def Let_def) 
31191  154 

155 
lemma (in term_syntax) term_of_nat_code [code]: 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

156 
"term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n" 
31191  157 
by (simp only: term_of_anything) 
158 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

159 
lemma (in term_syntax) term_of_code_numeral_code [code]: 
40884
3113fd4810bd
corrected representation for code_numeral numerals
haftmann
parents:
40883
diff
changeset

160 
"term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31191
diff
changeset

161 
by (simp only: term_of_anything) 
31191  162 

40883
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

163 
definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

164 
"term_of_num_ring two = (\<lambda>_. dummy_term)" 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

165 

b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

166 
lemma (in term_syntax) term_of_num_ring_code [code]: 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

167 
"term_of_num_ring two k = (if k = 0 then termify Int.Pls 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

168 
else if k = 1 then termify Int.Min 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

169 
else if k mod two = 0 then termify Int.Bit0 <\<cdot>> term_of_num_ring two (k div two) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

170 
else termify Int.Bit1 <\<cdot>> term_of_num_ring two (k div two))" 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

171 
by (auto simp add: term_of_anything Const_def App_def term_of_num_ring_def Let_def) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

172 

b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

173 
lemma (in term_syntax) term_of_int_code [code]: 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

174 
"term_of (k::int) = (if k = 0 then termify (0 :: int) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

175 
else termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num_ring (2::int) k)" 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

176 
by (simp only: term_of_anything) 
b37dca06477f
separate term_of function for integers  more canonical representation of negative integers
haftmann
parents:
40638
diff
changeset

177 

39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

178 

39564  179 
subsubsection {* Obfuscation *} 
31178  180 

181 
print_translation {* 

182 
let 

183 
val term = Const ("<TERM>", dummyT); 

184 
fun tr1' [_, _] = term; 

185 
fun tr2' [] = term; 

186 
in 

187 
[(@{const_syntax Const}, tr1'), 

188 
(@{const_syntax App}, tr1'), 

189 
(@{const_syntax dummy_term}, tr2')] 

190 
end 

191 
*} 

192 

193 

39564  194 
subsection {* Diagnostic *} 
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

195 

6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

196 
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where 
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

197 
[code del]: "tracing s x = x" 
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value  using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset

198 

33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

199 
code_const "tracing :: String.literal => 'a => 'a" 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

200 
(Eval "Code'_Evaluation.tracing") 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

201 

31178  202 

40638
6b137c96df07
adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
bulwahn
parents:
39567
diff
changeset

203 
hide_const dummy_term valapp 
42979
5b9e16259341
extending terms of Code_Evaluation by Free to allow partial terms
bulwahn
parents:
40884
diff
changeset

204 
hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring term_of_num_ring tracing 
28228  205 

206 
end 